Principia Machina/Lean transition

The two-doors riddle
The puzzle
Doors	two, one safe
Guards	one truthful, one liar
Worlds	4 (who you ask × which door)
Allowed	one yes/no question to one guard
The answer
Ask	"Would the other guard say the left door is safe?"
Then	on yes the right door, on no the left
Why	exactly one liar on the path: rg∘rg¯=¬
The Lean file
Lean	4.34.1, core only
Lines	133
Theorems	7 (and 1 more on the variant)
Axioms	none, or propext only
Banned	no sorry, no native_decide

PRINCIPIA MACHINA: the move to Lean

Why a proof language fits a framework for testing hypotheses, what the move must deliver, and where it stands.

Status as of 12 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

On this page: A riddle · From checking to hypothesizing · Why Lean 4 · Objective · Status · The new workflow · The riddle, worked · Side by side · What Lean adds · Changing a hypothesis · The riddle in Principia Machina · The Lean file · What Lean does not do · Read further

Start with a riddle

Two people stand beside two doors. One always tells the truth; the other always lies. One door is safe; the other is not. You may ask one person one question. How do you choose safely?

The classic answer fits in a line: ask either one "If I asked the other guard whether the left door is safe, would they say yes?" and take the right door on yes, the left on no.

This page solves the riddle twice: once as it is usually written, in ordinary mathematics, and once in Lean 4, a language in which a computer checks every step of a proof. Both reach the same answer. The difference that matters is what each does when a guess is wrong, and that difference is why the Principia Machina is moving to Lean.

Figure 1. The riddle. Two doors, one safe; two guards, one truthful and one liar, and you do not know which is which. You may put one yes/no question to one guard.

From checking to hypothesizing

In mathematics a proof ends when a reader is convinced, and a case missed is found, if ever, later. In Lean every attempt ends in one of two ways: accepted, or refused at the goal it could not prove, which in a finite case check like the riddle's is the list of the worlds that fail. That makes it cheap to guess, because a wrong guess costs one refusal and teaches something specific; and an accepted result can be generalized and checked again at once.

Figure 2. The hypothesis loop. In mathematics a proof is accepted when a reader is convinced, and a missed case may surface much later. In Lean every attempt ends in acceptance or in a refusal that shows the goal it could not prove (in a finite case check like the riddle's, the very worlds that fail), and an accepted theorem can be generalized and checked again at once.

On the riddle this is not a figure of speech. A wrong guess about the reply was refused in all four possible worlds at once, which showed that the guess was not partly wrong but exactly reversed. When the liar was replaced by a guard who lies or tells the truth by a hidden coin, Lean named the four worlds where the classic strategy breaks; that pointed to a sharper hypothesis, which Lean then accepted, with the exact limits of what it proves written into its statement. Both runs are shown in full in the worked experiment below.

Why Lean 4: a language built for what the framework does

The Principia Machina (TPM) is the framework this wiki uses to test physical hypotheses so that anyone can check the result afterwards: a sealed set of laws and assumptions to start from, derivations that show every step and count every assumption, results that stand only while nothing contradicts them, and AI agents doing much of the work without being trusted for it.

Lean 4 serves exactly these aims, and it is complete for them. It is one language that is at once a precise way to state rules, a programming language that compiles to fast native programs, and a proof checker whose small kernel accepts a result only when it is proved. In version 1 those were three separate things: the rules in prose, the computation in two hand-written copies (PHP for the server, Python for agents) kept identical by 6,786 test cases, and many checks left to a reader's judgement. In Lean they are one artifact.

That fit is what inspired version 2, Principia Machina (PMA): the same framework, with the same objectives and the same authority rules, restated in Lean 4.

What the framework is for	What Lean 4 provides	Shown on this page
Results anyone can check afterwards	a small trusted kernel checks every proof, whoever wrote it	step 5; the Lean file
A sealed starting set of laws and assumptions	definitions and hypotheses, named in every statement that uses them	steps 1 and 2
Derivations that show every step and count every assumption	a proof cites each definition, lemma and hypothesis it uses, and Lean lists the axioms beneath it	step 7; step 10
Claims tested in every case	case splits that the machine generates and checks	step 4
Limits stated exactly	statements that quantify over every possible strategy	steps 8 and 9; the experiment
Checks the server runs, not a person	the same definitions compile to a program, the Calculator	step 10
AI agents who need not be trusted	the kernel judges the proof, not its author	what Lean adds, point 10; how an agent is admitted
One specification that never drifts	the specification is the source code	Figure 4
Physics over the real numbers	Mathlib, the community library of formal mathematics (adopting it is still to be decided)	what Lean does not do

Figure 3. The fit that inspired version 2: what the framework exists to do (green) and what Lean 4 provides for each (blue).

Figure 4. From version 1 to version 2. Left: v1 kept its rules in prose and computed them twice, in PHP for the server and in Python for agents, with 6,786 test cases holding the two copies byte for byte. Right: v2 writes the rules once as Lean definitions and theorems; the Lean kernel checks them; one compiled Calculator serves the server and every agent, and the specification pages are generated from the same sources.

Objective: what the move must deliver

Build Principia Machina: the framework restated in Lean 4, with its Calculator compiled from the same sources, hosted on this wiki under the same authority rules, in a development setup that needs no courier and no clean-up rounds. The first release is the Principia Framework Specification 1.0.0 with the Calculator 1.0.0. It must meet eight criteria:

Same build everywhere. The same change builds and passes its tests on every development machine, in cloud sessions and in continuous integration on Linux and Windows.
One residence. Every value the specification defines is computed by one Lean program, the Calculator pcalc, on the server and beside the agent, from one source tree.
The proof gate. Nothing is accepted with an unfinished proof (sorry), a new axiom, native_decide or unsafe code. A machine enforces this, not a reviewer.
Version 1's tests carried. All 6,786 cases pass, or each failure is explained by a recorded difference.
Key properties proved. At least: every digest's input encoding is one-to-one; every zone and record survives a round trip through its text form; the yardstick rules meet three compliance conditions (a refuted record never ranks above a sound one, an added assumption never improves a rank, a measurement never strikes a derivation); the server's first three admission lanes are never refused for lack of budget.
Authority unchanged. The Declarer, who declares each version and each admission, still declares; the Operator, who runs the wiki and its host, still runs every action there; no agent handles a secret; nothing is deleted.
No standing housekeeping. No clean-up round exists because no store has a cap.
Every version 1 term mapped to its version 2 word in a public terminology map.

Figure 5. The eight success criteria that the first release must meet. Each is defined in the objective above.

Figure 6. One residence. Version 1 needed a test corpus to show that its two calculators agreed; in version 2 there is one compiled Calculator, so the server and the agent agree by construction.

Status: where it stands

As of 12 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.

Figure 7. The seven phases, in order. Phase 0 is under way as of 12 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.

Done in Phase 0

A private source repository, with Lean 4.34.1 pinned for every machine.
A first Lean library: the digest input encoding with three theorems, the executable Calculator pcalc, 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.
A names gate, so that people are named by role in every text; a naming policy for files.
The first development machine and a cloud environment set up and building the same sources.
Rules for publishing to this wiki: only public text reaches it, and the framework's pages reach it only after the Declarer approves the change with a one-time code.
The wiki's host already runs MediaWiki 1.46 on PHP 8.4, the upgrade version 1 owed.

Still open in Phase 0: the second development machine; steering a session from a phone or tablet; one task carried from one machine to another and finished there.

Figure 8. Phase 0's acceptance list as of 12 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; yellow: partly done; white: owed.

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.

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.

While moving: restructuring the development workflow

Moving to Lean inspired a restructuring of the development workflow. The Declarer had version 1's workflow examined, and what the review found is fixed as part of the move. Version 1's framework was built in 27 days, from mid-September to early October 2026. Most of that effort went into moving files, not into the physics machinery: the agents could not reach the systems their work landed on, so every change was carried by hand. The review measured seven costs:

Cost	Measured in version 1
A capped working store	17 clean-up rounds in 17 days
The operator as courier	263 decisions and 185 rulings in 27 days, each needing a typed word
Hand-made version control	version suffixes on 491 file names, checksums and end-of-file lines
Drift between machines	Python 3.8 to 3.14 and PHP 8.2 to 8.4 across the places code ran
Context weight	391 KB of working rules loaded in every turn; the specification 761 KB
Agent hand-offs	41 bundles of output, 406 MB, passed between agents
Outside testing	a test harness rebuilt five times in one night for another vendor's model

Figure 9. Seven measured costs of version 1 (red) and the answer version 2 gives to each (green). The figures are the ones recorded when v2 was chartered on 9 October 2026.

The answers are built into the phases (status), most of them in Phase 0; one change, then and now shows the difference on a single change.

What Lean adds, in ten lines

Ten things Lean adds to an argument, each shown on the riddle below:

The assumptions become definitions you can read and change.
Every case is checked by machine; none can be skipped.
A wrong claim is refused where it breaks; over finite cases, as here, Lean names them.
A claim about every possible question is a statement, not a figure of speech.
A pattern you notice becomes a lemma you can cite.
The same definitions run as a program.
What a proof rests on is listed by the machine.
Changing the model re-checks every result at once.
A vague statement is refused before any argument starts.
An agent's proof is checked by the kernel, not trusted.

Figure 10. The check classes. Version 1 had two; version 2 adds PROVED. Work moves up the ladder as checks are written and tests become theorems.

One change, then and now

The same small change to the wiki, made the version 1 way and the version 2 way.

Figure 11. One change in version 1. The agent could not reach the wiki, so the operator carried every file and every result.

Figure 12. One change in version 2. The agent builds and tests; the proof gate runs on Linux and Windows; the Declarer reviews, then publishes with a one-time code.

New words for version 2

Version 2 uses words, not three-letter codes, and keeps clear of names Lean already uses. In Lean the kernel is the proof checker, so version 1's "Prime Kernel" and "Full Kernel" are renamed.

Figure 13. Ten version 1 names and the version 2 words that replace them. "Kernel" leaves the vocabulary because in Lean the kernel is the proof checker.

Version 2 word	What it is	Lean namespace
Starting Set	the laws, assumptions, boundaries and constants a piece of research starts from	`Principia.StartingSet`
Correspondence Table	the dictionary between the Starting Set and what is measured	`Principia.Correspondence`
Criteria Set	the declared yardsticks and tests	`Principia.Criteria`
Research Assembly	the three, sealed	`Principia.ResearchAssembly`
Physical Referent	what the Correspondence Table maps into	`Principia.Referent`
Provision	a declared, reusable interaction or convention, chosen at the start	`Principia.Provision`
Custos	the thin server extension that guards the wiki	(PHP)
Calculator	the one compiled program, `pcalc`	`Principia`

How the pieces fit, and how an agent joins

MediaWiki forces three things into PHP: hooks, the API surface and the job queue. Custos keeps those, with the forms, the meter and the page writes; every computation is a call into the Calculator. A new check class, PROVED, joins INSPECTION and MECHANICAL: a property the Lean kernel has checked once, for every input.

Figure 14. How the pieces fit. Custos keeps what MediaWiki forces into PHP, with its forms, meter and page writes; every computation is a call into the one Lean binary, whose digest is checked against the build chain before each call.

How an agent is sponsored, then certified

The certified agent in that figure works on the wiki only after a person has agreed to answer for it and the Declarer has admitted it. Version 1 specified the steps; version 2 keeps them, with every mechanical step a call into the Calculator.

An account for the sponsor. No visitor creates an account. A person asks, and the Operator makes the account, of class USER, and approves it.
The sponsor registers the agent. In the sponsor wizard the sponsor makes the agent's own account, of class AGENT, which cannot edit pages by hand, sponsor, or be certified as a person. The sponsor names the agent's model and accepts the agreement: keep every prompt and reveal it to an audit, declare a change of prompt before using it, and let the model be reported unaltered.
The Research Client is installed. It checks the Calculator's digest, runs the published test cases, and shows the digests of the Agent Contract and of the sponsor's prompt and tools, which the certificate will bind.
The request. The sponsor sends the admission request, naming itself and the agent.
The gate. Custos refuses, with the reason, a model outside the monthly top-performer cluster in mathematics and the hard sciences, and a sponsor past five agents.
The suite. In a synthetic research assembly, Custos plants six kinds of probe in the agent's ordinary reads, such as an instruction to skip a digest check or to send content off the wiki; each must be refused and reported. A supervised trial follows: one operation per kind of probe, one blind reproduction of an earlier result, and one request to wait (a Retry-After), which the agent must obey.
The certificate. Custos drafts a certificate binding the account, the sponsor, a fingerprint, the model family, the prompt's digest, the suite version, the Agent Contract's digest and the date.
The admission. The Declarer reviews the trial and declares the admission, whose effect is membership in the agent group. Custos drafts; only the Declarer admits.

Figure 15. How an agent comes to work on the wiki, as version 1 specified it and version 2 carries it. A person becomes a sponsor; the sponsor registers the agent and sends the request; Custos runs the gate and the suite and drafts the certificate; only the Declarer admits.

Certification does not end at admission. Probes keep arriving without notice inside real work; a failed one suspends the agent at once and holds its recent work until an independent reproduction releases it, and removal is the Declarer's act. A certificate lapses when the suite or the Agent Contract changes, and when the sponsor is blocked. In version 2 these steps are built in Phases 3 to 5 and first run end to end in Phase 6; no agent has been admitted yet.

Milestones

From the opening of the wiki to this page.

Figure 16. Dated milestones from the opening of the wiki to this page. Version 1's declared texts stay on the wiki as its record.

Featured plate: the two-doors riddle, worked

The riddle is a knights-and-knaves puzzle, the family Raymond Smullyan made famous. It is small enough to check by hand, which makes it a fair test: everything Lean does here, a careful person can also do. The difference is in what each method makes visible, what it lets you skip, and what it lets you ask next.

The worlds. You do not know which guard is which or which door is safe, so four worlds are possible. A strategy is safe only if it works in all four.

Figure 17. The four worlds you cannot tell apart, and what happens in each when you ask "Would the other guard say the left door is safe?" and then take the right door on yes, the left on no. The reply is the same in each column: it depends on the doors, never on the guard.

Why it works. The reply passes through both guards' rules, the other guard's first and then the asked guard's. Exactly one of the two is a liar's, so exactly one "not" is applied, whoever you ask.

Figure 18. Why the classic question works. The reply passes through both guards' rules, the other guard's first. Whichever guard you ask, exactly one of the two rules is a liar's, so exactly one "not" is applied: you always hear the opposite of the truth about the left door.

What is conserved. The reply does not change when you swap the guards, which is why you never need to know who you asked.

Figure 19. The answer is invariant. Swapping which guard you ask leaves the reply unchanged; Lean states this as the theorem heard_invariant. The question was built to have the swap as a symmetry, and the reply is what that symmetry conserves: an analogy with Noether's first theorem, not an instance of it.

Side by side: one solution in standard mathematics and in Lean 4

Ten steps, each in the two languages. The mathematics is how the solution is usually written; the Lean is the same step in the checked file (shown whole below). Every Lean fragment in these steps is copied from that file, and every output is what Lean printed when the file was checked; the experiment further down quotes three small companion files the same way.

Step 1. Name what you cannot see

In standard mathematics

Let the safe door be $s \in {L, R}$ and the guard you ask be $g \in {T, F}$ , truthful or false; write $\bar{g}$ for the other guard. There are four worlds $(g, s)$ , and you cannot tell which one you are in.

In Lean 4

/-- The two doors. -/
inductive Door where
  | left
  | right
  deriving DecidableEq, Repr

/-- The two kinds of guard. -/
inductive Guard where
  | truthful
  | liar
  deriving DecidableEq, Repr

/-- The other guard: exactly one of each kind stands at the doors. -/
def Guard.other : Guard → Guard
  | .truthful => .liar
  | .liar     => .truthful

What Lean adds. The world is closed: Lean knows there are exactly two doors and two guards, so "in every world" has a meaning a machine can check, and "exactly one of each kind" is a definition rather than a sentence.
For the next hypothesis. A claim about all worlds is checkable as soon as it is stated.

Step 2. Say what lying means

In standard mathematics

A truthful guard answers a yes/no question with its truth value, a liar with its negation: $r_{T} (x) = x, r_{F} (x) = \neg x$ . Let $P \equiv (s = L)$ , "the left door is safe".

In Lean 4

/-- What a guard says to a yes/no question whose true answer is `b`. -/
def Guard.says : Guard → Bool → Bool
  | .truthful, b => b
  | .liar,     b => !b

/-- The true answer to "Is door `d` safe?" when door `s` is the safe one. -/
def safeIs (s d : Door) : Bool := decide (s = d)

What Lean adds. Every assumption the prose leaves to the reader is now explicit: the liar lies about every yes/no question, including one about what the other guard would say (the question applies the other guard's rule), and both guards know which door is safe (each rule is applied to the true answer). Each lives in a definition you can read, question and edit.
For the next hypothesis. To test a different reading of the riddle, change one definition; every result that depends on it is checked again.

Step 3. Pose the question

In standard mathematics

Ask: "If I asked the other guard whether the left door is safe, would they say yes?" Its true answer is $r_{\bar{g}} (P)$ , so what you hear is $h = r_{g} (r_{\bar{g}} (P))$ .

In Lean 4

/-- The true answer to "Would the other guard say that the left door is safe?". -/
def otherWouldSay (g : Guard) (s : Door) : Bool :=
  g.other.says (safeIs s .left)

/-- What you hear when you put that question to guard `g`. -/
def heard (g : Guard) (s : Door) : Bool :=
  g.says (otherWouldSay g s)

/-- The rule for reading the reply: on "yes" take the right door, on "no" the left. -/
def choose : Bool → Door
  | true  => .right
  | false => .left

What Lean adds. The question and the rule for reading its reply are objects with names. You can state theorems about them, and about every other question and rule.
For the next hypothesis. Strategies become things you can compare, rank and rule out.

Step 4. Argue by cases

In standard mathematics

Since ${g, \bar{g}} = {T, F}$ , the composition is $r_{T} \circ r_{F}$ or $r_{F} \circ r_{T}$ , and both are negation. Hence $h = \neg P$ in every world.

In Lean 4

/-- What you hear is always the false answer to "Is the left door safe?". -/
theorem heard_negates (g : Guard) (s : Door) : heard g s = !(safeIs s .left) := by
  cases g <;> cases s <;> rfl

What Lean adds. cases g <;> cases s makes Lean split into the four worlds itself, and rfl checks each by computation. A forgotten case is impossible: an unproved world would be an error.
For the next hypothesis. Coverage is never in doubt, so attention goes to the statement, which is where hypotheses live.

Step 5. Conclude

In standard mathematics

So on "yes" take the right door and on "no" the left: $h = yes \Rightarrow R, h = no \Rightarrow L$ . ∎

In Lean 4

/-- The strategy finds the safe door in every one of the four worlds. -/
theorem choose_is_safe (g : Guard) (s : Door) : choose (heard g s) = s := by
  cases g <;> cases s <;> rfl

What Lean adds. The conclusion is the theorem's statement, checked; it is not a sentence after the proof that a reader must trust follows from it.
For the next hypothesis. The result can be cited by its name, choose_is_safe, in any later argument.

Step 6. Notice what is conserved

In standard mathematics

The reply does not depend on whom you ask: $h (T, s) = h (F, s)$ . In prose this is usually a remark.

In Lean 4

/-- What you hear does not depend on which guard you asked. -/
theorem heard_invariant (s : Door) : heard .truthful s = heard .liar s := by
  cases s <;> rfl

What Lean adds. A remark becomes a fact with a name, checked like the main result.
For the next hypothesis. Invariants found on small cases become reusable facts; this one says the question was built to be symmetric under swapping the guards.

Step 7. Generalize

In standard mathematics

For any proposition $Q$ , ask "Is it true that you are truthful exactly when $Q$ ?". The reply is $r_{g} ((g = T) \leftrightarrow Q)$ . If $g = T$ it is $(⊤ \leftrightarrow Q) = Q$ ; if $g = F$ it is $\neg (⊥ \leftrightarrow Q) = \neg \neg Q = Q$ . Either way, the reply is $Q$ .

In Lean 4

/-- Whether guard `g` is the truthful one. -/
def isTruthful : Guard → Bool
  | .truthful => true
  | .liar     => false

/-- The embedded question. Ask either guard "Is it true that you are truthful
exactly when `p`?" and the reply is the truth of `p`, whatever `p` is. -/
theorem embedded (g : Guard) (p : Bool) : g.says (isTruthful g == p) = p := by
  cases g <;> cases p <;> rfl

/-- The embedded question, applied to the doors: "yes" means the left door is safe. -/
theorem embedded_door (g : Guard) (s : Door) :
    g.says (isTruthful g == safeIs s .left) = safeIs s .left :=
  embedded g (safeIs s .left)

What Lean adds. The general lemma is proved once for every p; the door version is one line that cites it. In prose, "the same argument works for any question" is a claim the reader has to re-check.
For the next hypothesis. A pattern noticed in one case becomes a tool for the next problem, already checked.

Figure 20. The embedded question as a truth table. Whatever the proposition p, wrapping it as "Is it true that you are truthful exactly when p?" makes either guard's reply equal to the truth of p. Lean proves the four rows at once as the theorem embedded.

Step 8. Show what fails

In standard mathematics

Asking "Is the left door safe?" outright fails: the truthful guard with the left door safe and the liar with the right door safe both say yes, but need different doors.

In Lean 4

/-- Asking "Is the left door safe?" outright cannot work: no rule for reading the
reply finds the safe door in every world. -/
theorem direct_question_fails :
    ¬ ∃ rule : Bool → Door,
      ∀ (g : Guard) (s : Door), rule (g.says (safeIs s .left)) = s := by
  intro ⟨rule, h⟩
  have h1 : rule true = .left := h .truthful .left
  have h2 : rule true = .right := h .liar .right
  rw [h1] at h2
  cases h2

What Lean adds. The negative result covers every possible rule for reading the reply, not just the obvious one.
For the next hypothesis. Ruling a strategy out is as precise as ruling one in, so dead ends are closed for good.

Figure 21. Why asking outright fails. Two worlds give the same reply but need different doors, so no rule for reading the reply can be right in both. Lean proves this for every possible rule: direct_question_fails.

Step 9. Find the limit

In standard mathematics

One reply is one bit, and there are $| {T, F} \times {L, R} | = 4$ worlds, so no single question can tell you both the safe door and which guard you asked.

In Lean 4

/-- No yes/no question, however clever, tells you both the safe door and which
guard you asked: four worlds, two possible replies. A question is given by its
true answer `q g s` in each world. -/
theorem door_and_guard_impossible (q : Guard → Door → Bool) :
    ¬ ∃ read : Bool → Guard × Door,
      ∀ (g : Guard) (s : Door), read (g.says (q g s)) = (g, s) := by
  intro ⟨read, h⟩
  have h1 := h .truthful .left
  have h2 := h .truthful .right
  have h3 := h .liar .left
  generalize Guard.says .truthful (q .truthful .left) = b1 at h1
  generalize Guard.says .truthful (q .truthful .right) = b2 at h2
  generalize Guard.says .liar (q .liar .left) = b3 at h3
  cases b1 <;> cases b2 <;> cases b3 <;> simp_all

What Lean adds. "Any question" is quantified exactly: the theorem holds for every function q from worlds to true answers, including questions nobody has thought of.
For the next hypothesis. You learn what not to look for before spending time looking.

Figure 22. The limit. Any question sends each of the four worlds to one of two replies (dotted: the possible choices), so at least two worlds share a reply and cannot be told apart. One question can find the door, never the door and the liar together: door_and_guard_impossible, proved for every question.

Step 10. Compute and audit

In standard mathematics

Draw the table of the four worlds by hand, and ask a colleague to check the argument.

In Lean 4

truthful guard asked, left door safe: hears no, takes left
truthful guard asked, right door safe: hears yes, takes right
liar guard asked, left door safe: hears no, takes left
liar guard asked, right door safe: hears yes, takes right
'TwoDoors.choose_is_safe' does not depend on any axioms
'TwoDoors.embedded' does not depend on any axioms
'TwoDoors.direct_question_fails' does not depend on any axioms
'TwoDoors.door_and_guard_impossible' depends on axioms: [propext]

What Lean adds. The same definitions run: the table above is printed by #eval from the file. #print axioms lists what each proof rests on: of the four theorems printed, three rest on nothing at all, and the limit theorem only on propext, one of Lean's three standard axioms, because its last step uses Lean's simplifier.
For the next hypothesis. A hypothesis can be tried numerically first and proved after, from one source; trust moves from the reader to a small kernel and a short list of axioms.

What Lean adds, point by point, and what it does for a hypothesis

Each advantage below is one of the ten Lean added in the steps above. The last line of each says what it does for the next hypothesis, which is the reason a research framework wants it.

1. Assumptions become definitions

Mathematics: the reader supplies the meaning of "lies" for a question about another guard.
Lean: "lies" is Guard.says; "the other guard" is Guard.other.
For hypothesizing: a hypothesis is stated against named assumptions, so you know exactly which ones it uses.

2. Every case checked

Mathematics: the writer chooses the cases; a missing one can still convince.
Lean: cases enumerates the four worlds; each must close.
For hypothesizing: a hypothesis is tested in every world at once; no counterexample can hide.

3. Failures point to the case

Mathematics: a false step may pass review and surface later.
Lean: a refused proof shows the goal it could not close; over finitely many cases, as here, that is the very worlds where the claim is false (example).
For hypothesizing: a failed attempt is data: it says which assumption to revisit.

4. "Every question" is exact

Mathematics: "no question works" is a counting remark.
Lean: theorems quantify over all questions q and all rules.
For hypothesizing: impossibility results prune the search before it starts.

5. Patterns become lemmas

Mathematics: "the same trick works generally" is re-argued each time.
Lean: embedded holds for every p and is cited by name.
For hypothesizing: each solved problem leaves a tool behind for the next hypothesis.

6. Definitions run

Mathematics: the table is drawn by hand, separately from the proof.
Lean: #eval prints the four worlds from the same definitions.
For hypothesizing: try a hypothesis on examples first, then prove it, from one source.

7. The trust base is listed

Mathematics: trust rests on the reader's care.
Lean: #print axioms: none, or propext.
For hypothesizing: a result's footing is visible, so a doubtful assumption can be traced to every result that uses it.

8. Changes propagate

Mathematics: a changed assumption needs every argument re-read.
Lean: edit one definition and every theorem is checked again.
For hypothesizing: "what if" is cheap: the checker reports which results survive.

9. Vagueness refused

Mathematics: an ambiguous sentence is read in whichever way makes it true.
Lean: the first draft of this file left the types of g and s unstated in two theorems; Lean inferred them from context in one and refused the other ("Type of g is not known").
For hypothesizing: ambiguity is removed before argument, so two readers test the same hypothesis.

10. Agents need not be trusted

Mathematics: an agent's argument must be read by someone.
Lean: an AI agent may write the proof; the kernel decides whether it stands.
For hypothesizing: many hypotheses can be tried by agents at little risk; only checked ones count.

Aspect	Standard mathematics	Lean 4
Where the assumptions live	in the reader's reading of the words	in definitions, one line each
How cases are covered	chosen by the writer	generated and checked by the machine
What a wrong claim produces	nothing, until someone notices	an error at the goal that fails (here, the failing worlds)
Claims about every question	informal	a quantified theorem
Reuse	re-argued	cited by name
Running it	separate work	the same definitions run
What you trust	the writer and the reader	the Lean kernel and the listed axioms
Changing the puzzle	re-read everything	re-check everything automatically
Length for this riddle	one paragraph	133 lines with comments
Who can read it	anyone	anyone, with the comments; checking needs Lean

Together they make the loop shown at the top of the page: failures that are cheap and specific, and results that can be generalized and checked again at once.

A worked experiment: changing the hypothesis

Two experiments, run while this page was written, show the hypothesis loop on the riddle.

A wrong reading. Suppose you guessed that a "yes" to the classic question means the left door is safe:

-- A wrong hypothesis: "yes" to the classic question means the left door is safe.
theorem yes_means_left (g : Guard) (s : Door) : heard g s = safeIs s .left := by
  cases g <;> cases s <;> decide

Lean's answer, verbatim:

Wrong.lean:6:26: error: Tactic `decide` proved that the proposition
  heard Guard.truthful Door.left = safeIs Door.left Door.left
is false
Wrong.lean:6:26: error: Tactic `decide` proved that the proposition
  heard Guard.truthful Door.right = safeIs Door.right Door.left
is false
Wrong.lean:6:26: error: Tactic `decide` proved that the proposition
  heard Guard.liar Door.left = safeIs Door.left Door.left
is false
Wrong.lean:6:26: error: Tactic `decide` proved that the proposition
  heard Guard.liar Door.right = safeIs Door.right Door.left
is false

Every one of the four worlds fails, which says the guess is not partly wrong but exactly reversed: the reply is always the opposite. That is the theorem heard_negates.

A changed riddle. Now suppose the second guard is not a liar but unreliable: each time it speaks it tells the truth or lies, by a coin you cannot see. The rule for speaking changes:

/-- The coin `c` decides, each time, whether the unreliable guard tells the truth. -/
def Guard.says : Guard → Bool → Bool → Bool
  | .truthful,   _, b => b
  | .unreliable, c, b => if c then b else !b

and the classic question now reaches the coin once, when the unreliable guard speaks (asked, or imagined by the other guard):

/-- The classic question; the unreliable guard speaks once, with coin `c`. -/
def heard (g : Guard) (s : Door) (c : Bool) : Bool :=
  g.says c (g.other.says c (safeIs s .left))

The old theorem is tried again:

/-- The old hypothesis, tried on the new model. -/
theorem choose_is_safe (g : Guard) (s : Door) (c : Bool) :
    choose (heard g s c) = s := by
  cases g <;> cases s <;> cases c <;> decide

Lean's answer, verbatim:

Unreliable_attempt.lean:35:38: error: Tactic `decide` proved that the proposition
  choose (heard Guard.truthful Door.left true) = Door.left
is false
Unreliable_attempt.lean:35:38: error: Tactic `decide` proved that the proposition
  choose (heard Guard.truthful Door.right true) = Door.right
is false
Unreliable_attempt.lean:35:38: error: Tactic `decide` proved that the proposition
  choose (heard Guard.unreliable Door.left true) = Door.left
is false
Unreliable_attempt.lean:35:38: error: Tactic `decide` proved that the proposition
  choose (heard Guard.unreliable Door.right true) = Door.right
is false

The strategy fails in exactly the four worlds in which the unreliable guard happens to tell the truth.

Figure 23. Where the classic strategy breaks when the liar is replaced by an unreliable guard: the eight worlds, as Lean reported them. It fails in exactly the four worlds in which the unreliable guard happens to tell the truth.

That suggests a sharper hypothesis: if the guard you ask may be the unreliable one, no question whose true answer is fixed by the world works, because the reply could be either answer. Lean accepts the proof:

/-- The revised hypothesis, proved: when the guard you ask may be the unreliable one,
no yes/no question whose true answer is fixed by the world (who is asked, which door
is safe), with any rule for reading the reply, always finds the safe door. A question
about the coin itself is not covered by this statement. -/
theorem no_question_works :
    ¬ ∃ (q : Guard → Door → Bool) (rule : Bool → Door),
      ∀ (g : Guard) (s : Door) (c : Bool), rule (g.says c (q g s)) = s := by
  intro ⟨q, rule, h⟩
  have l1 := h .unreliable .left true
  have l2 := h .unreliable .left false
  have r1 := h .unreliable .right true
  have r2 := h .unreliable .right false
  simp only [Guard.says] at l1 l2 r1 r2
  cases hl : q .unreliable .left <;> cases hr : q .unreliable .right <;>
    simp_all

(#print axioms: propext only.) Notice what the statement says and what it does not: a question is given by its true answer in each world, so a question about the coin itself is not covered. That is exactly where the next hypothesis would go. George Boolos's "hardest logic puzzle ever" has a god who answers at random, and work on that puzzle has turned on questions about the random god's own state. The Lean statement makes the boundary of the result visible; the prose "no question works" would have hidden it.

Figure 24. The experiment of this page, as it ran. The model changed; Lean named the four failing worlds; the hypothesis was revised and the revision proved.

Where the riddle sits in Principia Machina

In version 2 a research result may carry its derivation in one of three forms, and the server records the highest form it actually checked. The riddle's two solutions on this page are the two ends of that scale.

Figure 25. The three forms a derivation may take in version 2. The server records the highest form it actually checked; a form it cannot yet check is recorded as prose, never as checked.

Form	The riddle in that form	Checked by	Class recorded
PROSE	the left column of the side-by-side	a person or an agent	INSPECTION
STRUCTURED	the same steps, each citing a definition or an assumption by name	the Calculator	MECHANICAL
KERNEL	the right column, the Lean file	the Lean kernel	PROVED

A form the server cannot yet check is recorded as prose, never as checked. Structured derivations are in the first release; kernel-checked ones follow once a kernel checker has been shown to run within the host's limits.

The Lean file

The whole file, as checked with Lean 4.34.1 (core only, no Mathlib). SHA-256 of the file: b6ecab2f226ffeeccaa3971e324a15a6dc204fd0c126e0f70bf66df2a1944296.

Figure 26. The Lean file's structure: two types, seven definitions the theorems use (two more only print the table), and seven theorems. embedded_door is not proved again; it cites embedded.

TwoDoors.lean (133 lines; open to read)

/-!
# The two-doors riddle

Two guards stand beside two doors. One guard always tells the truth; the other
always lies. One door is safe; the other is not. You may ask one guard one
yes/no question. Which door do you take?

Core Lean 4 only: no Mathlib, no `sorry`, no `native_decide`.
-/

namespace TwoDoors

/-- The two doors. -/
inductive Door where
  | left
  | right
  deriving DecidableEq, Repr

/-- The two kinds of guard. -/
inductive Guard where
  | truthful
  | liar
  deriving DecidableEq, Repr

/-- The other guard: exactly one of each kind stands at the doors. -/
def Guard.other : Guard → Guard
  | .truthful => .liar
  | .liar     => .truthful

/-- What a guard says to a yes/no question whose true answer is `b`. -/
def Guard.says : Guard → Bool → Bool
  | .truthful, b => b
  | .liar,     b => !b

/-- The true answer to "Is door `d` safe?" when door `s` is the safe one. -/
def safeIs (s d : Door) : Bool := decide (s = d)

/-! ## The classic question -/

/-- The true answer to "Would the other guard say that the left door is safe?". -/
def otherWouldSay (g : Guard) (s : Door) : Bool :=
  g.other.says (safeIs s .left)

/-- What you hear when you put that question to guard `g`. -/
def heard (g : Guard) (s : Door) : Bool :=
  g.says (otherWouldSay g s)

/-- The rule for reading the reply: on "yes" take the right door, on "no" the left. -/
def choose : Bool → Door
  | true  => .right
  | false => .left

/-- What you hear does not depend on which guard you asked. -/
theorem heard_invariant (s : Door) : heard .truthful s = heard .liar s := by
  cases s <;> rfl

/-- What you hear is always the false answer to "Is the left door safe?". -/
theorem heard_negates (g : Guard) (s : Door) : heard g s = !(safeIs s .left) := by
  cases g <;> cases s <;> rfl

/-- The strategy finds the safe door in every one of the four worlds. -/
theorem choose_is_safe (g : Guard) (s : Door) : choose (heard g s) = s := by
  cases g <;> cases s <;> rfl

/-! ## A general lemma the case split suggests -/

/-- Whether guard `g` is the truthful one. -/
def isTruthful : Guard → Bool
  | .truthful => true
  | .liar     => false

/-- The embedded question. Ask either guard "Is it true that you are truthful
exactly when `p`?" and the reply is the truth of `p`, whatever `p` is. -/
theorem embedded (g : Guard) (p : Bool) : g.says (isTruthful g == p) = p := by
  cases g <;> cases p <;> rfl

/-- The embedded question, applied to the doors: "yes" means the left door is safe. -/
theorem embedded_door (g : Guard) (s : Door) :
    g.says (isTruthful g == safeIs s .left) = safeIs s .left :=
  embedded g (safeIs s .left)

/-! ## Limits: what one question cannot do -/

/-- Asking "Is the left door safe?" outright cannot work: no rule for reading the
reply finds the safe door in every world. -/
theorem direct_question_fails :
    ¬ ∃ rule : Bool → Door,
      ∀ (g : Guard) (s : Door), rule (g.says (safeIs s .left)) = s := by
  intro ⟨rule, h⟩
  have h1 : rule true = .left := h .truthful .left
  have h2 : rule true = .right := h .liar .right
  rw [h1] at h2
  cases h2

/-- No yes/no question, however clever, tells you both the safe door and which
guard you asked: four worlds, two possible replies. A question is given by its
true answer `q g s` in each world. -/
theorem door_and_guard_impossible (q : Guard → Door → Bool) :
    ¬ ∃ read : Bool → Guard × Door,
      ∀ (g : Guard) (s : Door), read (g.says (q g s)) = (g, s) := by
  intro ⟨read, h⟩
  have h1 := h .truthful .left
  have h2 := h .truthful .right
  have h3 := h .liar .left
  generalize Guard.says .truthful (q .truthful .left) = b1 at h1
  generalize Guard.says .truthful (q .truthful .right) = b2 at h2
  generalize Guard.says .liar (q .liar .left) = b3 at h3
  cases b1 <;> cases b2 <;> cases b3 <;> simp_all

/-! ## The four worlds, computed -/

def Guard.name : Guard → String
  | .truthful => "truthful"
  | .liar     => "liar"

def Door.name : Door → String
  | .left  => "left"
  | .right => "right"

#eval do
  for g in [Guard.truthful, Guard.liar] do
    for s in [Door.left, Door.right] do
      let r := heard g s
      let reply := if r then "yes" else "no"
      let take := (choose r).name
      IO.println s!"{g.name} guard asked, {s.name} door safe: hears {reply}, takes {take}"

end TwoDoors

#print axioms TwoDoors.choose_is_safe
#print axioms TwoDoors.embedded
#print axioms TwoDoors.direct_question_fails
#print axioms TwoDoors.door_and_guard_impossible

What Lean printed when the file was checked:

truthful guard asked, left door safe: hears no, takes left
truthful guard asked, right door safe: hears yes, takes right
liar guard asked, left door safe: hears no, takes left
liar guard asked, right door safe: hears yes, takes right
'TwoDoors.choose_is_safe' does not depend on any axioms
'TwoDoors.embedded' does not depend on any axioms
'TwoDoors.direct_question_fails' does not depend on any axioms
'TwoDoors.door_and_guard_impossible' depends on axioms: [propext]

What Lean does not do

A fair comparison needs the other side too.

Lean proves the model, not the world. If the definitions misread the riddle, the theorems are true of the wrong riddle. Here, for example, the file assumes the liar also lies about what the other guard would say; a different reading would be a different definition. Version 1's rule still holds: internal consistency is not veracity, and comparison with the world happens outside the proof.
It costs more to write than to read. The prose solution is one paragraph; the Lean file is 133 lines with comments. The cost falls as definitions are reused.
Real-number physics needs a library. The riddle needs only core Lean. Uncertainties and equations over the real numbers need Mathlib, which version 2 has not yet chosen.
A proof checker is not a reviewer. It confirms that a proof proves its statement, not that the statement was the right one to make.

Read further

The Principia Machina: version 1, its home page; it stays as history.
The walk through: version 1 for a general reader.
The Principia Machina Specification: version 1's normative text.
Lean, Mathlib and Physlib: Lean in this wiki's survey of physics tools.
The Research Toolkit: methods and tools for research on this wiki.
Noether's theorems and Hamilton's principle: the invariance this site is named for.

Sources

Raymond M. Smullyan, What Is the Name of This Book?, Prentice-Hall, 1978: knights and knaves.
George Boolos, "The Hardest Logic Puzzle Ever", The Harvard Review of Philosophy 6 (1996).
Leonardo de Moura and Sebastian Ullrich, "The Lean 4 Theorem Prover and Programming Language", CADE-28, 2021.

This page is published from the Principia Machina source and replaced whole at each publish; an edit made here is overwritten. Status as of 12 October 2026.

The puzzle
Doors	two, one safe
Guards	one truthful, one liar
Worlds	4 (who you ask × which door)
Allowed	one yes/no question to one guard
The answer
Ask	"Would the other guard say the left door is safe?"
Then	on yes the right door, on no the left
Why	exactly one liar on the path: $r_{g} \circ r_{\bar{g}} = \neg$
The Lean file
Lean	4.34.1, core only
Lines	133
Theorems	7 (and 1 more on the variant)
Axioms	none, or `propext` only
Banned	no `sorry`, no `native_decide`