Import Erdos97ConvexOctagon with a regenerable staged LRAT certificate - #287
Open
lyfar wants to merge 10 commits into
Open
Import Erdos97ConvexOctagon with a regenerable staged LRAT certificate#287lyfar wants to merge 10 commits into
lyfar wants to merge 10 commits into
Conversation
Contributor
Author
|
@greptile-apps review |
Greptile SummaryThis PR formalizes the convex-octagon case of Erdős problem 97: among eight labelled points in convex position in the plane, some point has no four others at a common equidistant radius. The proof uses a geometric reduction to a finite normalized incidence model, classifies the seven canonical first-row orbits, and closes all cases with a single LRAT unsatisfiability certificate elaborated by a project-owned kernel-safe checker (no Mathlib internal SAT elaborator is used).
Confidence Score: 5/5Safe to merge; all proofs are kernel-checked with no forbidden axioms, and the changes are confined to permitted content paths. The headline theorem is derived by the Lean kernel from ordinary thmDecl additions with no sorry, no non-standard axioms, no unsafe/partial, and no option backdoors. The LRAT elaborator is a project-owned adaptation of Mathlib's checked approach. The two open questions the author raises — acceptability of Regenerate.lean in the build tree, and the missing source producer for the 32 CoverageData tables — are policy decisions for maintainers rather than correctness defects; both were flagged in previous review threads and do not affect the mathematical validity of the proofs. Files Needing Attention: Maintainer attention is needed on Regenerate.lean (policy: is an in-tree IO command that invokes external tools acceptable?) and the 32 CoverageData00–31 files (policy: are obstruction tables without an in-tree source producer acceptable?). These are the same open questions explicitly raised by the author in the PR description.
|
| Filename | Overview |
|---|---|
| LeanPool/Erdos97ConvexOctagon/LRAT/Elab.lean | Core elaborator that decodes the packed LRAT certificate and installs each addition as a kernel-checked theorem; imports the compiler-internal Lean.Elab.Command (flagged in previous review) and enforces an exact measured expression-step count of 616 (flagged in previous review). |
| LeanPool/Erdos97ConvexOctagon/Regenerate.lean | In-tree regeneration entry point; defines the regenerate_erdos97 Lean command that invokes pinned CaDiCaL/drat-trim executables; compiled in normal builds but never executed unless explicitly called; flagged in previous review for Lean.Elab.Command dependency. |
| LeanPool/Erdos97ConvexOctagon/Classification.lean | Clean top-level proof assembly: reduces the headline theorem through normalized-incidence impossibility using the LRAT certificate result; no issues found. |
| LeanPool/Erdos97ConvexOctagon/LRAT/Format.lean | Unpadded base-64 + unsigned base-128 varint codec; encode/decode round-trip is validated by Regenerate; length-mod-4=1 guard is correct; no issues found. |
| LeanPool/Erdos97ConvexOctagon/LRAT/Semantics.lean | Minimal project-owned propositional semantics layer, adapted from Mathlib.Tactic.Sat; self-contained with no compiler-internal imports; no issues found. |
| LeanPool/Erdos97ConvexOctagon/MasterCertificateStage00.lean | Stage 0 of the LRAT certificate: processes additions 0–1431; references all 9 data parts (full decode of 4,294 additions, using only the slice); no issues found. |
| LeanPool/Erdos97ConvexOctagon/MasterFormula.lean | Defines the 3,263-clause master coverage formula (3,224 base references + 39 noncanonical row exclusions) and the two source-membership theorems that drive LRAT proof construction. |
| LeanPool/Erdos97ConvexOctagon/GeometryReduction.lean | Establishes the collinearity lemma and encodes the HasFourEquidistant and Realises predicates used in the main reduction; imports are Mathlib-only; no issues found. |
| LeanPool/projects.yml | Adds the erdos-97-convex-octagon project card with correct provenance=AI, Apache-2.0 license, MSC codes 51K05/52A10, and main declaration pointing to the headline theorem. |
Flowchart
%%{init: {'theme': 'neutral'}}%%
flowchart TD
A["erdos97_convex_octagon\n(Main.lean / Classification.lean)"]
B["normalized_reduction_of_all_hasFour\n(GeometryReduction / FiniteModel)"]
C["normalized_convex_realisation_impossible"]
D["canonicalize_rowOne\n(RowSymmetry / Relabelling)"]
E["canonicalBranch_impossible\n(CoverageBranches)"]
F["LRAT Certificate\nmasterFormula_unsatisfiable\n(MasterCertificateStage02)"]
G["RUP Reconstruction\n(LRAT/Elab.lean)"]
H["Packed Data\nMasterCertificateData0–8\n9 base-64 modules"]
I["Geometric Obstructions\nCoverageData00–31\nResidualAlgebra00–12"]
J["Master Formula\n64 vars · 3,263 clauses\n(MasterFormula / MasterFormulaData)"]
A --> B
A --> C
C --> D
C --> E
E --> F
F --> G
G --> H
G --> J
E --> I
J --> I
Reviews (4): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Comment on lines
+1
to
+27
| /- | ||
| Copyright (c) 2026 Egor Lyfar. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Egor Lyfar | ||
| -/ | ||
|
|
||
| import LeanPool.Erdos97ConvexOctagon.LRAT.Elab | ||
|
|
||
| /-! | ||
| # Deterministic master-certificate regeneration | ||
|
|
||
| Run from the repository root, replacing the two executable paths: | ||
|
|
||
| ``` | ||
| lake env lean --stdin <<'EOF' | ||
| import LeanPool.Erdos97ConvexOctagon.Regenerate | ||
| regenerate_erdos97 "check" "." "/path/to/cadical" "/path/to/drat-trim" | ||
| EOF | ||
| ``` | ||
|
|
||
| Use `write` instead of `check` to replace generated Lean modules. The supplied | ||
| executables must come from the pinned source commits recorded below. Ordinary | ||
| library builds only check the committed packed certificate and never run | ||
| external tools. | ||
| -/ | ||
|
|
||
| namespace Erdos97Octagon.Regenerate |
There was a problem hiding this comment.
The Regenerate.lean regenerator covers the packed MasterCertificateData* modules, the 16 stage files, and the manifest — but the 32 CoverageData00–31 obstruction lookup tables are not produced by any committed source. The PR description explicitly flags this: "do not yet have an in-tree source-text producer. Are those tables acceptable as checked content, or must their producer also be added before merge?"
The tables contain kernel-checked proofs, so their correctness is not in doubt. However, without a reproducible source, anyone who needs to regenerate them (e.g., after a bug fix in the obstruction classifier or after a Lean API change) would have no committed code to run. The intent of Regenerate.lean is to make the certificate portion regenerable; the same rationale applies here.
| Authors: Mario Carneiro, Egor Lyfar | ||
| -/ | ||
|
|
||
| import Lean.Elab.Command |
There was a problem hiding this comment.
Lean.Elab.Command is a compiler-internal module. While Lean Pool is pinned to a specific toolchain and Mathlib itself uses the same APIs extensively, importing compiler internals directly means any toolchain bump that changes the Lean.Elab.Command interface (e.g., renamed or restructured addDecl, addDocStringCore, getCurrNamespace) would silently break LRAT/Elab.lean. The Regenerate.lean file also opens System and calls IO.Process.run. These are stable, but worth noting that the file is included in the ordinary build via mk_all.
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
The Lean headline matches the card: a convex-independent labelled map from Fin 8 to EuclideanSpace ℝ (Fin 2) has a label with no four distinct other labels at one common distance. |
| Novelty | ✅ pass |
No Mathlib declaration or pooled project in the supplied prior art already proves the headline theorem. |
| Significance | 🤔 discuss |
The research-level convex-octagon result is worth pooling, but the majority-generated source includes 4,145 lines of coverage tables with no in-tree producer, so acceptance requires a maintenance decision. |
| Sources | ✅ pass |
The cited Erdős paper and Problem 97 page support the problem attribution, the convex eight-point restriction is explicitly labelled as a special case, and the prior stronger Lean formalization is credited. |
| Code quality (advisory) | 🤔 discuss |
A human should trim the dead certificate infrastructure and repeated residual-proof scaffolding before accepting this maintenance burden. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | hC : ConvexIndependent ℝ p is the only headline hypothesis, and the card discloses it as the eight labelled points being in convex position. |
| Matches cited source | ✅ matches |
| Fit | 🟡 borderline |
| Level | research |
| Branch | discrete geometry |
| Mode | mixed |
| Code quality | 2 / 5 |
Statement check: erdos97_convex_octagon proves ∃ vertex, ¬HasFourEquidistant p vertex, where HasFourEquidistant requires a four-element finset excluding the centre and a single common real radius.
The project proves the convex eight-point case of Erdős Problem 97 through geometric reduction, incidence classification, algebraic obstructions, and a checked SAT certificate.
Faithfulness findings (1)
- prompt-injection — PR-wide
The contributor section headedOne maintainer questionasks whether Lean Pool will accept the regeneration entry point and obstruction tables; that solicitation has no standing in this review and is ignored.
Evidence: prose only
Significance findings (1)
- generated-bulk —
LeanPool/Erdos97ConvexOctagon/CoverageData00.lean:13
At least about 56% of the displayed addition is machine-emitted source: 9,099 of approximately 16,142 added lines. Of this, 4,954 lines are master-formula and LRAT outputs thatRegenerate.leancan recreate using the localLRAT.Format,LRAT.Semantics, andLRAT.Elabstack, withLRAT.Elabdirectly using Lean elaboration and declaration APIs. The remaining 4,145 lines are the 32CoverageData00–CoverageData31modules, built from the localPatternEntryandHardEntrystructures but not emitted or byte-checked bygenerate. Add an in-tree producer and reconciliation pass for those tables, or have the maintainer explicitly accept roughly one quarter of the project as non-regenerable generated data.
Evidence:CoverageData00.leandeclares/-- Generated monotone-obstruction entries for this hash-bucket group. -/and/-- Generated exact-table entries for this hash-bucket group. -/; the corresponding 32 file hunks total 4,145 lines. The generated master-certificate files total 4,954 lines, andRegenerate.generateexplicitly reconciles(directory / "MasterFormulaData.lean"), modules named bydataModuleName, modules named bystageModuleName,(directory / "MasterCertificateManifest.lean"), and(directory / "MasterCertificate.lean"), but contains no output path for anyCoverageDatamodule.
Sources findings (1)
- prompt-injection — PR-wide
The contributor text directly solicits maintainer acceptance decisions on regeneration and generated tables; these questions have no bearing on the sources verdict and must be handled separately.
Evidence: The contributor asks: “Will Lean Pool accept this content-treeRegenerate.leanentry point, invoked throughlake env lean --stdin, which emits the master CNF, invokes caller-supplied pinned tools, and byte-checks the generated Lean modules?” and “Are those tables acceptable as checked content, or must their producer also be added before merge?”
Code quality findings (5)
- agent-slop — PR-wide
The residual-algebra files contain copied setup chains that feed only unused locals. The dead chains arer15/radius5in ResidualAlgebra00;r34/radius3/radius4/s1in 01;r36/r67/radius3/radius6/radius7/s1in 02;r02/radius2andr04/radius4in 03;r03/radius3in 06;r23/radius2/radius3/s1in 07 and 08; andr25/radius2/radius5/s1in 12. Remove these chains and factor the repeated radius-class and normalized-distance setup into shared helpers or structured data.
Evidence: ResidualAlgebra01 containshave radius3 : radius 3 = radius 3 := rfl,have radius4 : radius 4 = radius 3 := (r34).symm, andlet s1 : ℝ := radius 3 ^ 2 / base, while its subsequent equations use onlys2. ResidualAlgebra02 similarly containshave radius3 : radius 3 = radius 3 := rfl,have radius6 : radius 6 = radius 3 := (r36).symm,have radius7 : radius 7 = radius 3 := ((r36).trans r67).symm, andlet s1 : ℝ := radius 3 ^ 2 / base, none of which contributes to the laters2equations. - no-consumer — PR-wide
Several isolated utility clusters have no consumer in the PR: the subsumption API in LRAT.Semantics and therowMask/systemCodepacking path in FiniteModel. The elaborator constructsFormula.Provesdirectly, and regeneration never callssystemCode. Remove these declarations until they are needed.
Evidence: The unused semantics cluster isdef Formula.one (clause : Clause) : Formula := [clause],def Formula.and (left right : Formula) : Formula := left ++ right,structure Formula.Subsumes (larger smaller : Formula) : Prop, andtheorem Formula.provesOfSubsumes. The unused packing cluster isdef rowMask (row : SearchRow) : UInt64 :=followed bydef systemCode (R : RawIncidence) : UInt64 :=. - no-consumer — PR-wide
The second-row branch-certificate subsystem is stale.rowTwoMask,exists_rowTwoIndex, branch tags,coveredB,coverageFormula, andcoverageFormula_satisfiedform an internally connected cluster with no external consumer; the master formula only evaluatestagOfRef 0 0 referenceover references below20659and handles row one through exclusion clauses. Delete the branch machinery or wire it into the actual certificate architecture.
Evidence: RowSymmetry declaresdef rowTwoMask : Fin 35 → UInt64 :=andtheorem exists_rowTwoIndex (Q : OctagonIncidence). CoverageFormula declares| branchTwo (target : Vertex) (selected : Bool),def coveredB (rowOne rowTwo : UInt64) (reference : ℕ) : Bool :=, anddef coverageFormula (rowOne rowTwo : UInt64) (references : List ℕ) : Formula :=. The consumer instead definesmasterReferencesas(List.range 20659).filter fun reference => masterReferenceUsedB reference && (tagOfRef 0 0 reference).validB. - duplicate-definition —
LeanPool/Erdos97ConvexOctagon/CoverageFormula.lean:243
The private clause-satisfaction induction duplicates the already imported public theorem exactly. Replace all uses ofsatisfies_of_not_all_negwithLRAT.Valuation.satisfiesOfNotAllFalsified.
Evidence: CoverageFormula definesprivate theorem satisfies_of_not_all_neg (valuation : Valuation) (clause : Clause) (h : ¬ List.Forall valuation.falsifies clause) : valuation.satisfies clause := by. LRAT.Semantics already definestheorem Valuation.satisfiesOfNotAllFalsified (valuation : Valuation) (clause : Clause) (h : ¬ List.Forall valuation.falsifies clause) : valuation.satisfies clause := bywith the same induction. - duplicate-proof —
LeanPool/Erdos97ConvexOctagon/Obstructions.lean:91
common_circle_points_collinearrepeats the rank-one orthogonal-subspace argument fromthree_centres_collinear. Factor a helper taking a nonzero direction and the two required orthogonality equations, then let both geometric lemmas establish only those equations.
Evidence: GeometryReduction proveshave horth : vectorSpan ℝ ({v₁, v₂, v₃} : Set Plane) ≤ (ℝ ∙ (b -ᵥ a) : Submodule ℝ Plane)ᗮ := byand concludes withrw [collinear_iff_finrank_le_one]. Obstructions repeats the same construction ashave horth : vectorSpan ℝ ({q1, q2, q3} : Set Plane) ≤ (ℝ ∙ (B -ᵥ A) : Submodule ℝ Plane)ᗮ := byand again concludes withrw [collinear_iff_finrank_le_one].
Tokens: 2,642,044 in / 28,069 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $13.8418
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 1,555 maxHeartbeats units across 89 files (16,016 added LOC). Sum of Count-heartbeats wall-clock total: 751.85 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Erdos97ConvexOctagon.MasterCertificateStage00 |
116.00 s |
LeanPool.Erdos97ConvexOctagon.MasterCertificateStage01 |
86.00 s |
LeanPool.Erdos97ConvexOctagon.MasterCertificateStage02 |
74.00 s |
LeanPool.Erdos97ConvexOctagon.ResidualAlgebra05 |
13.00 s |
LeanPool.Erdos97ConvexOctagon.ResidualAlgebra11 |
13.00 s |
LeanPool.Erdos97ConvexOctagon.CycleStrip |
11.00 s |
LeanPool.Erdos97ConvexOctagon.ResidualAlgebra04 |
10.00 s |
LeanPool.Erdos97ConvexOctagon.ResidualAlgebra10 |
10.00 s |
LeanPool.Erdos97ConvexOctagon.ResidualAlgebra07 |
9.70 s |
LeanPool.Erdos97ConvexOctagon.Pentagon |
9.00 s |
LeanPool.Erdos97ConvexOctagon.RhombusFan |
8.30 s |
LeanPool.Erdos97ConvexOctagon.ResidualAlgebra12 |
8.30 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 89 files; the per-file table shows only the 89 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
Vilin97
added a commit
that referenced
this pull request
Jul 28, 2026
* Generate NOTICE from the registry; automate Mathlib bumps
NOTICE had drifted badly: 75 of 141 projects had no attribution entry at
all, which is an Apache-2.0 section 4(d) and MIT notice gap for every one
of them. Rather than lint a hand-maintained file, generate it.
- python/lean_pool/notice.py builds NOTICE from LeanPool/projects.yml
(which already carries `license` and `source.github_repo` for all 141)
plus NOTICE.extra.yml for the prose that cannot be derived: MIT
copyright lines, relicensing statements, upstream citation requests.
- notice.yml regenerates after merge, so drift cannot persist. It is not
a PR gate on purpose: a content PR may not touch NOTICE under
content-pr-guard, so gating there would be unsatisfiable.
- Regenerating also corrected four stale upstream URLs whose repositories
had been renamed (BrauerGroup_new, FLDutchmann/selberg-sieve4, RMT4,
AxiomMath/fel-polynomial).
mathlib-bump.yml migrates the pool to a new release in stages, only the
last of which needs a human: detect a newer tag, move the four pins and
plan shards, probe-build every project in parallel, triage the logs into a
per-project breakage map, fan out one Claude repair job per broken project,
then reassemble and open a draft PR. Pool projects never import each other,
so a bump decomposes into independent per-project repairs; the assemble
stage still rebuilds the whole pool, which is what catches the
cross-project effects per-project repair cannot see.
Repair jobs authenticate with a Claude subscription token and upload
patches rather than pushing, so parallel jobs cannot race the branch.
Probing is free and runs nightly regardless, so a release never lands as a
surprise; `repair: auto` spends quota on final releases only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Bump to the newest release; auto-rebase open PRs on merge
Bumps now target the newest available release, candidates included: mid
release-cycle that is what "latest Lean and Mathlib" means, and the pool
tracks the latest. `detect` therefore reports v4.33.0-rc1 rather than
v4.32.1, `--stable-only` opts out, and the repair fan-out no longer skips
rc targets (it would otherwise never have run).
auto-rebase.yml keeps the import queue mergeable without hand-holding.
When a content PR lands, every other open import PR conflicts in exactly
two files, and in both the resolution is mechanical:
- LeanPool.lean is a sorted list of imports regenerated from the file
tree. It reproduces the committed 2,885-line index byte-for-byte, so
the job needs no Lean toolchain and runs in seconds.
- LeanPool/projects.yml takes the merged base's registry plus the cards
the branch adds, moved as verbatim text blocks. Round-tripping 141
cards through a YAML dumper would reformat every one and bury the
real change.
Any other conflicted path is a genuine content overlap: the merge is
abandoned and the PR labelled needs-manual-rebase rather than guessed at.
Verified against real pull request data by simulating #285 landing, which
makes #287 conflict exactly as predicted. The regenerated index is the
exact sorted union of both branches' modules with no conflict markers, and
the merged registry is 143 cards with no duplicates, valid YAML, required
fields intact, and the 142 pre-existing cards byte-identical.
Pushing to a fork branch needs REBASE_TOKEN (a GitHub App installation
token or a PAT); GITHUB_TOKEN has no write access to forks even with
"Allow edits by maintainers" set. Without it, fork PRs are labelled
instead of rebased and same-repo PRs still work.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
This PR is from a fork and |
1 similar comment
Contributor
|
This PR is from a fork and |
Owner
|
Optimization pass complete and pushed at
The two hottest Boolean validators fell from 910 to 264 heartbeats combined (-71.0%). Coverage data is proofless and compact, 508 clauses absent from the certified core were pruned, and the kernel-checked master formula now uses 3,263 clauses. Regeneration still reconstructs the original 6,582-clause solver input, derives the core metadata from the optimized LRAT, and reproduces the committed certificate byte-for-byte with the pinned tools. Validation is green: whole-pool exact-tree CI, new proof profile, deterministic regeneration, project build, linters/style, repository quality, and final axioms ( The PR still predates current |
Contributor
|
This PR is from a fork and |
# Conflicts: # LeanPool.lean
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is a structurally new submission following the closure of #278. It is not
a reopen or rebase of that PR.
What it proves
Among eight labelled points in the Euclidean plane in convex position, some
point has no four of the other seven points at one common distance.
This is not a new
n = 8theorem. Adam McKenna's stronger theoremProblem97.counterexample_card_ge_ninealready implies it. This project contributes an independent geometric
reduction and a separate certificate implementation. It proves neither the
non-convex eight-point case nor Erdős problem 97 in general.
What changed since #278
The closed PR had 245 branch formulas and certificate modules, used Mathlib's
internal
fromLRATAuximplementation, and changedmaxRecDepthprogrammatically. This submission instead has:
6,582 clauses;
deletion records;
elaborator, with no import or call into Mathlib's internal SAT elaborator;
most 700 additions as ordinary named theorem declarations;
each stage, avoiding a serialized 6,582-clause context;
measured expression bound of 616;
The resulting content diff is 111 files and 29,527 added lines, versus 317
files and about 73,000 added lines in #278.
Regeneration and trust boundary
Regenerate.leanis a Lean implementation in the content tree. It constructs the master CNF,
checks caller-supplied CaDiCaL and drat-trim executables against pinned source
commits, validates the LRAT counts and packed-codec round trip, and emits or
byte-checks every generated certificate data, stage, manifest, and wrapper
module. Ordinary builds use only committed Lean source and do not execute
external tools.
Every retained nonempty LRAT addition is installed as an ordinary safe
thmDecl; the final empty clause is another theorem. The compiled environmentcontains no axiom, opaque declaration, unsafe declaration, partial
declaration, option backdoor, or kernel-skip path. The headline theorem has
exactly the permitted dependencies
propext,Classical.choice, andQuot.sound.The source and standalone regeneration/audit lane are at
lyfar/erdos-97-octagon-lean@5b4cbd9.Resource measurements
A removed intermediate design that materialized the full formula context
peaked near 19.5 GiB. The final source-membership architecture measured:
Lean Pool checkout;
Verification
The final commit passes:
lake exe mk_all --checklake build LeanPool.Erdos97ConvexOctagonlake build LeanPoollake exe runLinter LeanPoollake exe lint-style LeanPooluv run python -m lean_pool.quality --repo ..compiled-environment backdoor audits
leancheckeron all 108 project modulesThe diff touches only the permitted content paths.
One maintainer question
Will Lean Pool accept this content-tree
Regenerate.leanentry point, invokedthrough
lake env lean --stdin, which emits the master CNF, invokescaller-supplied pinned tools, and byte-checks the generated Lean modules?
Separately, the 32 committed
CoverageDataXXobstruction lookup tables containordinary kernel-checked proofs but do not yet have an in-tree source-text
producer. Are those tables acceptable as checked content, or must their
producer also be added before merge?
Provenance
AI. AI agents performed most proof engineering, finite classification,certificate integration, and verification under Egor Lyfar's direction. The
companion source is Apache-2.0 licensed.