Principia Machina/Progress/Phase 1

Principia Machina: map
Reading the program The move to Lean Status Terminology: the words of both versions
Lean itself Lean theorem prover Principia Machina in Lean
Version 1 The Principia Machina its specification

Phase 1: foundations

Goal: what the port to Lean stands on. The tests that settle how the wiki's server runs the Calculator (T1 to T3, then T5); version 1's material copied into the source repository; the register of words; the declared parameters and the record table in Lean, with the three forms a derivation may take; and the push that keeps these pages current. Phase 1 began beside Phase 0, which remains the current focus.

Done

• 2026-10-14: begun beside Phase 0. Test T1 and the first half of version 1's seed, done earlier the same day, are recorded on Phase 0's page.
• 2026-10-14: version 1's 33 vector corpora, 6,786 test cases in all, and the 33 programs that generated them, copied verbatim from the version 1 tree published on this wiki. Every file was checked against the digests published with that tree, and the tree's own digest against the value the project already held from version 1's records. They test version 1's functions, which the port takes up in Phase 2.
• 2026-10-14: the declared parameters and tuning options of version 1's specification, in Lean: 146 definitions, a structure of 133 tuning options holding version 1's starting values, and 36 theorems on the constraints the specification states. Every value is exact, with no floating point. Where the sources leave a value or its class open, the question is put to the Declarer.
• 2026-10-14: the terminology page: every version 1 term beside its version 2 word, its proposed three-letter code, its Lean namespace and the rule behind the choice, generated from the terminology map with a check that refuses any difference between the two. The codes are shown as proposed until the Declarer approves them. It reaches the wiki at the next publish.
• 2026-10-14: the record table as Lean types, with the three forms a derivation may take (prose, structured steps, a Lean proof) and the class each earns: a form is credited only when its checker accepted that derivation, and an unchecked form earns nothing.
• 2026-10-14: a map for every section of the wiki, after the one version 1's pages carry: a box of reading links that stays with the reader through the pages they walk, on Hamilton's principle, Noether's theorems, On Physical Lines of Force, the Research Toolkit, the Lean theorem prover edition and these pages. Every page in those walks shows its own name as its title, and the Main Page gains an entrance to the Lean edition beside the other editions. It reaches the wiki at the next publish, and gates no item of any phase.
• 2026-10-14: the terminology page went up on the wiki with the Declarer's publish, its codes marked proposed until he approves them.
• 2026-10-15: the 22 physics tool pages show their tool's name as their title, not their place in the wiki's tree. It reaches the wiki at the next publish.
• 2026-10-15: the Research Toolkit's chart on the Main Page fits its column at every width; it had spilled past its box on narrow screens. It reaches the wiki at the next publish.
• 2026-10-15: version 1's calculator library, the 25 Python files its corpus generators import, and the 31 input files they read, copied verbatim from the version 1 tree published on this wiki, so those generators now run from the source repository. Every file was checked against the digests published with that tree. Run against them, all 30 generators that write a corpus reproduce theirs byte for byte.
• 2026-10-15: the survey of Lean's toolchain, built. It reads Lean's newest versions, Lean's list of supported platforms and the versions of the tools the automatic checks use, quotes each source as served, and compares them with the versions the project has fixed; on a newer version it prepares the change, which the automatic checks test before the Declarer accepts it. Lean's known gaps (Unicode normalization, SHA-256, the order of keys in Lean's JSON objects) are checked against Lean's own notes and reported, never changed. Its first run found Lean 4.35.0, newer than the 4.34.1 the project uses; that upgrade comes as a change of its own. The monthly run waits on the Declarer, who sets it up.
• 2026-10-15: test T5's run on the wiki's host became a step of the Operator's closing run, as the runs of T1 to T3 are: it waits on test T1's pass, reads the checker's time and verdict against the test's pass line, and skips itself once the result is recorded. The step that makes the account for these pages searches wider for the wiki's installation on its host, names what it finds, and keeps the one it is given or finds. Test T3's run from one scheduled run stays the Operator's, set by hand.
• 2026-10-15: the closing run now lands what the Operator's run produces on this page and on the status panel too, each item once, the figure of the phases redrawn when a state changes. A new step of it copies version 1's named texts still missing from the Operator's own copy: the six specification texts, the declarations files and the full sources of version 1's server extension and research client, each checked against the digest the project holds where it holds one, for the Declarer to read before anything is merged.
• 2026-10-15: the Declarer approved the three-letter code table as it stands.
• 2026-10-15: the terminology page and the terminology map show the three-letter codes as approved. The page's rule on Mathlib's words now says that version 2 is written in Lean's core alone for now, by the Declarer's choice. It reaches the wiki at the next publish.
• 2026-10-16: the first unattended push of these pages, by that account; from now on they are pushed after every landing and compared with the wiki once a day.
• 2026-10-17: the survey of Lean's toolchain set to run once a month, on the 22nd, as a scheduled task of its own: when Lean serves a newer version it proposes the change, which the automatic checks test before the Declarer accepts it.
• 2026-10-17: test T2 on the wiki's host, under MediaWiki's shell framework from the command line: one call with a 1 MB JSON document took 0.070 CPU-seconds and 72 ms (pass: under 2 CPU-seconds): PASS.
• 2026-10-17: test T3 on the wiki's host, from the shell: 100 calls in one run took 7.432 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: PASS; its scheduled run follows.
• 2026-10-15: the closing run can now set up test T3's scheduled run on the wiki's host itself, as the Declarer chose, when the Operator asks it to: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.
• 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.
• 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
• 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
• 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
• 2026-10-18: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.

Open

• The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.

Next

Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

as of 2026-10-19