Repository navigation
Nothing in this repository builds the Lean proofs #2747
Description
proofs/lean4/ holds a lakefile.lean and 250 completeness theorems. Across 45 workflow files, not one runs lake build, installs elan, or references proofs/lean4 at all:
$ ls .github/workflows/*.yml | wc -l
45
$ grep -rlE "lake build|lake exe|elan|leanprover|lean4" .github/workflows/*.yml
(no matches)
The three files that match a bare lean are two type: boolean lines and a Rust test name.
So every by native_decide in this tree is a claim no instrument has checked since whoever last ran Lean by hand.
What that is already covering for
- 40 of the 250 theorems are about an EMPTY module — no functions, no globals, no tests.
native_decideproves the empty module is lowerable, which is true and true of nothing in the spec the theorem is named after. These are now recorded indocs/reports/lean_completeness_mismatches.jsonundermax_vacuous, with a ratchet that only moves down (Five checks that had stopped describing the code they guard #2744 added the ledger, this issue's companion PR adds the second ratchet). - 73 of the theorems disagree with the Rust classifier. Until recently the test comparing them aborted on the first, so it had been reporting 1.
- There is no generator. 250
Env/Modulepairs were transcribed by hand, and nothing in the tree can re-derive them from the specs, so a transcription error is invisible and permanent.
Why this issue rather than a fix
Adding a lake build job is the fix, and it is the kind that must be run before it is landed: Lean is not installed on the machine this was found on, so whether the 250 theorems still compile is unknown here. Landing a job that may be red on master at the end of an unattended session is the wrong trade; landing it after one local lake build is the right one.
The job, ready to paste:
name: Lean proofs
on:
pull_request:
paths: ["proofs/lean4/**"]
push:
branches: [master]
paths: ["proofs/lean4/**"]
workflow_dispatch:
jobs:
lake:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: leanprover/lean-action@v1
with:
lake-package-directory: proofs/lean4Note the paths: filter. A gate with paths: and no unfiltered push: runs zero times on master, so "it does not fail on master" would mean "it has never run there" — add workflow_dispatch (above) and fire it once against master to get the missing measurement before trusting the green.
What the fix should also decide
Whether Stmt.forLoop gets a second constructor. It has one for both range-for and iterator-for and asks only that the range expression be combinational, so it cannot express the construct that makes specs/ar/asp_solver.t27 non-lowerable — which is why that spec is pinned to the Rust verdict by a marker rather than modelled.
Boundary
specs/ar/asp_solver.t27
Activity
A theorem about an empty module may not multiply (#2751)
docs(now): skill sections 134-137
Four lessons from closing #2743 and the seal gate (#2752)
Make the unmeasured measurable: workflow_dispatch on twenty gates, an…
fix(lean): unfold the definitions the positivity lemmas could not see
fix(lean): seesaw_ordering had its bullets in the wrong order
fix(lean): four more real-valued definitions marked noncomputable
fix(lean): the last two goals -- bounds on e/pi, and a crude bound fo…
fix(lean): the division lemmas carry a zero suffix in this mathlib
fix(lean): two-decimal pi bounds, and Koide left as one named failure
docs(lean): stop guessing lemma names down a four-minute loop
gHashTag commentedon Aug 28, 2026
The measurement was taken. The proofs did not build.
lean-proofs.ymllanded in #2759 and was dispatched againstmaster— the firstlake buildthis repository has ever run. It failed, and the failures were real:NeutrinoMasses.leandefs over ℝ markednoncomputableunfold—norm_numdoes not unfold adef, so it never saw thath_H4is 30NeutrinoMasses.leanclean; build moved on toH4Lagrangian.leannoncomputable, andseesaw_ordering's bullets were in the wrong order fordiv_lt_div_of_pos_rightThree classes, all of them genuine: definitions over the reals that cannot compile without the marker, tactics that could not unfold a
defto reach a constant, and one proof whose bullets did not match its lemma's argument order.The two that remain, and why they are not fixed here
Both statements are true, with room to spare:
L01_lagrangian_order_of_magnitudeKoide_H4_testL01needs a bound one/π, and two decimal places suffice:0.8 × 3.15 = 2.52 < eand0.9 × 3.14 = 2.826 > e. Four names were tried, one CI round each —Real.pi_gt_3141592,Real.pi_lt_31415927,Real.pi_gt_314,Real.pi_lt_315— all unknown here, whileReal.pi_posandReal.exp_one_gt_d9resolve. The bounds most likely sit behind an import this file does not have.Koideneeds only0 < K < 4/3, sinceK = 789/t²andt² > 591.75follows from the crudest root bounds. An attempt reached a rewrite that found no occurrence — theletbindings inKoide_H4do not reduce the way the tactic assumed.Guessing lemma names down a four-minute feedback loop is the wrong instrument. Someone with the mathlib API in front of them closes both in a minute, and the comments in the file now say exactly what each needs and what was already tried.
One thing worth keeping from the attempts
lt_div_iffanddiv_lt_iffdo not resolve in this revision;lt_div_iff₀anddiv_lt_iff₀do. Recorded in the file.Still open from the original issue
native_decideproves the empty module lowerable, which says nothing about the spec each is named after. Held from growing bymax_vacuousindocs/reports/lean_completeness_mismatches.json.Completeness.lean— 250 models transcribed by hand, nothing that can re-derive them.Stmt.forLoophas one constructor for both range-for and iterator-for, so the Ast cannot express what makesspecs/ar/asp_solver.t27non-lowerable.push:tolean-proofs.yml— deliberately absent until a dispatch comes back green. Two errors away.docs(now): the first lake build, and what it said
The first lake build this repository ever ran: 28 errors to 2 (#2761)
gHashTag commentedon Aug 29, 2026
Measured: 114 of the 250 completeness theorems are about an empty module, and the ratchet counts 44.
Completeness.leanfunctions := []Envtoomax_vacuousmax_vacuousreadslean_completeness_mismatches.json, and an entry only reaches that ledger if the model also disagrees with the Rust classifier. Whether a theorem is vacuous has nothing to do with whether the classifier happens to disagree — so the ratchet built to stop vacuous theorems growing sees less than half of them.All 44 of its marks are correct: zero entries marked
model_emptythat are not empty. This is a coverage gap, not a wrong reading.tri lean vacuousreports all five numbers (#2890), and refuses rather than printing zero if it matches no modules — a zero from a scanner that found nothing is indistinguishable from a clean file.Why I am not fixing any of them
I proposed writing real models for four of these and did not.
lean,lakeandelanare not installed on this machine;.github/workflows/lean-proofs.ymlhas alake build, so the instrument exists but not where I am.And a faithful model may make its theorem false —
t27c gen-rust specs/github/auth.t27exits 1 and emits 0 lines, so the classifier says those specs do not lower. An honest transcription might therefore be unprovable, which would be the correct outcome and not a bug. I cannot tell that outcome apart from my own transcription error without building it.That is the shape of this issue: nothing in the repository builds these proofs, so the only thing holding 250 hand-written models to reality is whether a person transcribed correctly — and for 114 of them the transcription is empty.
tri lean vacuous: the ratchet counts 44 of 114 (#2890)
skill(ci-gates) 340-341: the wrong population, and the proof I did no…
gHashTag commentedon Sep 23, 2026
A boundary drafted from the paths this issue already names, so a bee can take it. Nothing is reserved until this is in the issue body - the Queen reads the body, not comments. Check the paths first: a wrong boundary reserves files the work does not own.
Boundary
specs/ar/asp_solver.t27docs/reports/lean_completeness_mismatches.jsondocs: the coordination entry this branch needs to land
Nothing in this repository builds the Lean proofs (#4732)
fix(specs): #5968 comment-swallowed commas in swarm_agents/autonomous…
docs: ledger the ml_transformer_multi_head_attention lean/rust split …