PMA Publisher: Published from the Principia Machina source

2026-10-15T19:30:10Z

Published from the Principia Machina source

← Older revision		Revision as of 19:30, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:The move to Lean}}		{{DISPLAYTITLE:The move to Lean}}
			{{Principia Machina map}}
	<noinclude><!-- Principia Machina: the transition to Lean. Published from the Principia Machina source; the whole page is replaced at each publish. Box styles inline, as on the Main Page. --></noinclude><templatestyles src="Principia Machina/styles.css" />		<noinclude><!-- Principia Machina: the transition to Lean. Published from the Principia Machina source; the whole page is replaced at each publish. Box styles inline, as on the Main Page. --></noinclude><templatestyles src="Principia Machina/styles.css" />

Line 259:		Line 260:
	P0 [label="Phase 0 The development setup\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];		P0 [label="Phase 0 The development setup\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];
	P1 [label="Phase 1 Foundations\nunder way", fillcolor="#cedff2", color="#6a8fbf"];		P1 [label="Phase 1 Foundations\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
	P2 [label="Phase 2 The Calculator\~~nnot started~~"];		P2 [label="Phase 2 The Calculator\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
	P3 [label="Phase 3 Custos\nnot started"];		P3 [label="Phase 3 Custos\nnot started"];
	P4 [label="Phase 4 The Research Client\nnot started"];		P4 [label="Phase 4 The Research Client\nnot started"];
Line 269:		Line 270:
	</graphviz>		</graphviz>
	</div>		</div>
	<div id="lt-fig-7" style="font-size: 0.88em; color: #54595d; margin: 0 0 0.9em 0;">'''Figure 7.''' The seven phases, in order, drawn from the status panel: Phases 0 ~~and 1~~ under way; Phases 2 to 6 not started. The current focus is Phase 0, the lowest phase not done. A phase may begin before the one before it is done. Every state is written in its box; the colours repeat it: green, done; blue, under way; grey, not started; a heavier outline, the current focus.</div>		<div id="lt-fig-7" style="font-size: 0.88em; color: #54595d; margin: 0 0 0.9em 0;">'''Figure 7.''' The seven phases, in order, drawn from the status panel: Phases 0 to 2 under way; Phases 3 to 6 not started. The current focus is Phase 0, the lowest phase not done. A phase may begin before the one before it is done. Every state is written in its box; the colours repeat it: green, done; blue, under way; grey, not started; a heavier outline, the current focus.</div>
	'''Done in Phase 0'''		'''Done in Phase 0'''
	* A private source repository, with Lean '''4.34.1''' pinned for every machine.		* A private source repository, with Lean '''4.35.0''' pinned for every machine.
	* A first Lean library: the digest input encoding with three theorems, the executable Calculator <code>pcalc</code>, and a test runner over the first corpus (6 cases, all passing).		* A first Lean library: the digest input encoding with three theorems, the executable Calculator <code>pcalc</code>, and a test runner over the first corpus (6 cases, all passing).
	* The proof gate: an audit of the axioms behind every declaration (7 checked, 0 failures), on Linux and Windows.		* The proof gate: an audit of the axioms behind every declaration (7 checked, 0 failures), on Linux and Windows.

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:00:41Z

Published from the Principia Machina source

← Older revision		Revision as of 18:00, 14 October 2026
Line 1:		Line 1:
			{{DISPLAYTITLE:The move to Lean}}
	<noinclude><!-- Principia Machina: the transition to Lean. Published from the Principia Machina source; the whole page is replaced at each publish. Box styles inline, as on the Main Page. --></noinclude><templatestyles src="Principia Machina/styles.css" />		<noinclude><!-- Principia Machina: the transition to Lean. Published from the Principia Machina source; the whole page is replaced at each publish. Box styles inline, as on the Main Page. --></noinclude><templatestyles src="Principia Machina/styles.css" />

Line 4:		Line 5:
	<div id="lt-welcome" style="font-size: 1.8em; line-height: 1.3; padding: 0.1em;">PRINCIPIA MACHINA: the move to Lean</div>		<div id="lt-welcome" style="font-size: 1.8em; line-height: 1.3; padding: 0.1em;">PRINCIPIA MACHINA: the move to Lean</div>
	<div style="font-size: 0.95em;">Why a proof language fits a framework for testing hypotheses, what the move must deliver, and where it stands.</div>		<div style="font-size: 0.95em;">Why a proof language fits a framework for testing hypotheses, what the move must deliver, and where it stands.</div>
	<div style="font-size: 0.85em; margin-top: 0.3em;">Status as of 13 October 2026 · Phase 0, the first of seven, under way · version 1, [[The Principia Machina]], stays at its titles as history · 26 figures on this page</div>		<div style="font-size: 0.85em; margin-top: 0.3em;">Status as of 14 October 2026 · Phase 0, the first of seven, under way · version 1, [[The Principia Machina]], stays at its titles as history · 26 figures on this page</div>
	</div>		</div>

Line 247:		Line 248:
	<h2 id="lt-status-h2" style="margin: 0; padding: 8px 10px; background-color: #eaecf0; border-bottom: 1px solid #a2a9b1; font-size: 1.2em; font-weight: bold;">Status: where it stands</h2>		<h2 id="lt-status-h2" style="margin: 0; padding: 8px 10px; background-color: #eaecf0; border-bottom: 1px solid #a2a9b1; font-size: 1.2em; font-weight: bold;">Status: where it stands</h2>
	<div id="lt-status" style="padding: 10px;">		<div id="lt-status" style="padding: 10px;">
	'''As of 13 October 2026: Phase 0, the development setup, is under way. No physics machinery has been ported yet, by design:''' beyond one small module used as ~~the~~ test subject (the digest input encoding), the ~~setup has to pass~~ its ~~acceptance list first~~.		'''As of 14 October 2026: Phase 0, the development setup, is under way. No physics machinery has been ported yet, by design:''' Phase 0 ports nothing from version 1 beyond one small module used as its test subject (the digest input encoding); the port itself is the work of Phase 2, the Calculator. Every item of every phase, with its state and its projected date, is a lamp on the [[Principia Machina/Progress/Status\|status panel]], from which Figure 7 is drawn.

	<div class="pma-fig" style="text-align: center; overflow-x: auto; margin: 0.6em 0 0.2em 0;">		<div class="pma-fig" style="text-align: center; overflow-x: auto; margin: 0.6em 0 0.2em 0;">
Line 256:		Line 257:
	edge [color="#54595d", fontname="Helvetica", fontsize=9, fontcolor="#202122", arrowsize=0.7];		edge [color="#54595d", fontname="Helvetica", fontsize=9, fontcolor="#202122", arrowsize=0.7];
	node [width=3.6];		node [width=3.6];
	P0 [label="Phase 0 The development setup\~~nUNDER WAY~~", fillcolor="#~~8fd1b4~~", color="#~~14866d~~", penwidth=1.6];		P0 [label="Phase 0 The development setup\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];
	P1 [label="Phase 1 Foundations\~~nnot started~~"];		P1 [label="Phase 1 Foundations\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
	P2 [label="Phase 2 The Calculator\nnot started"];		P2 [label="Phase 2 The Calculator\nnot started"];
	P3 [label="Phase 3 Custos\nnot started"];		P3 [label="Phase 3 Custos\nnot started"];
Line 268:		Line 269:
	</graphviz>		</graphviz>
	</div>		</div>
	<div id="lt-fig-7" style="font-size: 0.88em; color: #54595d; margin: 0 0 0.9em 0;">'''Figure 7.''' The seven phases, in order. Phase 0 is under way ~~as of 13 October 2026~~; ~~beyond one small module used as the test subject~~, ~~nothing from version 1 is ported until~~ the ~~development setup passes its acceptance list~~.</div>		<div id="lt-fig-7" style="font-size: 0.88em; color: #54595d; margin: 0 0 0.9em 0;">'''Figure 7.''' The seven phases, in order, drawn from the status panel: Phases 0 and 1 under way; Phases 2 to 6 not started. The current focus is Phase 0, the lowest phase not done. A phase may begin before the one before it is done. Every state is written in its box; the colours repeat it: green, done; blue, under way; grey, not started; a heavier outline, the current focus.</div>
	'''Done in Phase 0'''		'''Done in Phase 0'''
	* A private source repository, with Lean '''4.34.1''' pinned for every machine.		* A private source repository, with Lean '''4.34.1''' pinned for every machine.
Line 288:		Line 289:
	T [label=<<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="5" COLOR="#a2a9b1">		T [label=<<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="5" COLOR="#a2a9b1">
	<TR><TD BGCOLOR="#eaecf0" ALIGN="LEFT"><B>Phase 0 acceptance item</B></TD><TD BGCOLOR="#eaecf0"><B>State</B></TD></TR>		<TR><TD BGCOLOR="#eaecf0" ALIGN="LEFT"><B>Phase 0 acceptance item</B></TD><TD BGCOLOR="#eaecf0"><B>State</B></TD></TR>
	<TR><TD ALIGN="LEFT">1 One change builds alike everywhere</TD><TD BGCOLOR="#~~cef2e0~~">3 of 4 places</TD></TR>		<TR><TD ALIGN="LEFT">1 One change builds alike everywhere</TD><TD BGCOLOR="#cedff2">under way: 3 of 4 places</TD></TR>
	<TR><TD ALIGN="LEFT">2 Start a task in one place, finish it in another</TD><TD BGCOLOR="#~~8fd1b4~~"><B>done</B></TD></TR>		<TR><TD ALIGN="LEFT">2 Start a task in one place, finish it in another</TD><TD BGCOLOR="#cef2e0"><B>done</B></TD></TR>
	<TR><TD ALIGN="LEFT">3 Steer a session from a phone or tablet</TD><TD BGCOLOR="#~~ffffff~~">owed</TD></TR>		<TR><TD ALIGN="LEFT">3 Steer a session from a phone or tablet</TD><TD BGCOLOR="#eaecf0">owed</TD></TR>
	<TR><TD ALIGN="LEFT">4 Read a broken proof through the AI's Lean tools</TD><TD BGCOLOR="#~~cef2e0~~">2 of 3 places</TD></TR>		<TR><TD ALIGN="LEFT">4 Read a broken proof through the AI's Lean tools</TD><TD BGCOLOR="#cedff2">under way: 2 of 3 places</TD></TR>
	<TR><TD ALIGN="LEFT">5 Line endings identical from Windows and Linux</TD><TD BGCOLOR="#~~8fd1b4~~"><B>done</B></TD></TR>		<TR><TD ALIGN="LEFT">5 Line endings identical from Windows and Linux</TD><TD BGCOLOR="#cef2e0"><B>done</B></TD></TR>
	</TABLE>>];		</TABLE>>];
	}		}
	</graphviz>		</graphviz>
	</div>		</div>
	<div id="lt-fig-8" style="font-size: 0.88em; color: #54595d; margin: 0 0 0.9em 0;">'''Figure 8.''' Phase 0's acceptance list as of 13 October 2026. Item 4 means reading Lean's errors through the tools an AI agent uses, not a pasted terminal. ~~Green~~: done ~~or mostly done~~; ~~white:~~ owed.</div>		<div id="lt-fig-8" style="font-size: 0.88em; color: #54595d; margin: 0 0 0.9em 0;">'''Figure 8.''' Phase 0's acceptance list as of 14 October 2026. Item 4 means reading Lean's errors through the tools an AI agent uses, not a pasted terminal. Every state is written in its cell; the colours repeat it: green, done; blue, under way; grey, owed and not yet started.</div>
	'''Next''': ~~Phase 1 begins with test~~ T1~~, which runs a~~ Lean program on the wiki's own server from PHP. If it ~~passes~~, ~~one~~ Calculator serves both sides. ~~If it fails~~, ~~Lean stays~~ the ~~oracle~~ that ~~proves and generates test vectors~~, and ~~PHP and Python remain~~ the ~~runtime~~.		'''Next''': Test T1 has run. A Lean program built on a development machine runs on the wiki's own server, both when started from the server's command line and when started by PHP run there as a command. It does not start inside a web request: the host gives a web worker about a twentieth of the memory range it gives a command-line program, which is less than the Lean runtime claims when it starts, and that claim does not shrink when the program is told to use a single processor thread. One Calculator therefore still serves both sides, as [[#lt-fig-4\|Figure 4]] describes, and Custos calls it outside the web request rather than during it. The two tests after T1 run on the same server: T2 times one call with a one-megabyte input, started the way the wiki starts the program that draws its diagrams, and T3 measures what a hundred calls in one scheduled run cost against the processor time the host allows each hour.

	'''Questions still to decide''': core Lean or the Mathlib library (Mathlib brings real-number analysis, at the cost of a 2 to 3 GB build cache); how SHA-256 and Unicode normalization are provided; the table of three-letter codes; and the order in which the server's admission controls are built.		'''Questions still to decide''': core Lean or the Mathlib library (Mathlib brings real-number analysis, at the cost of a 2 to 3 GB build cache); how SHA-256 and Unicode normalization are provided; the table of three-letter codes; and the order in which the server's admission controls are built.
Line 1,487:		Line 1,488:
	* Leonardo de Moura and Sebastian Ullrich, "The Lean 4 Theorem Prover and Programming Language", CADE-28, 2021.		* Leonardo de Moura and Sebastian Ullrich, "The Lean 4 Theorem Prover and Programming Language", CADE-28, 2021.

	<small>This page is published from the Principia Machina source and replaced whole at each publish; an edit made here is overwritten. Status as of 13 October 2026.</small>		<small>This page is published from the Principia Machina source and replaced whole at each publish; an edit made here is overwritten. Status as of 14 October 2026.</small>
	</div>		</div>
	</div>		</div>

PMA Publisher: Published from the Principia Machina source

2026-10-13T13:29:32Z

Published from the Principia Machina source

Show changes

PMA Publisher: Published from the Principia Machina source

2026-10-13T07:28:02Z

Published from the Principia Machina source

Show changes

Principia Machina/Lean transition - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source