Repository navigation
Exposition: minimal Lean files + per-project viewer facet counts - #282
Merged
Merged
Conversation
Every declaration panel gains a "Minimal Lean file" button (next to the dependency cone): a standalone .lean file with the declaration's statement cone — definitions keep their bodies, theorem proofs are replaced by `sorry` — opened directly in the Lean 4 web playground (LZ-compressed #codez= link, verified against lean4web's decoder), with download and copy fallbacks. Assembly happens client-side from per-project shards plus raw sources fetched at the shard's pinned commit; nothing is pregenerated. - Extractor: statement-only dependencies (`tdeps`) per theorem, so the minimal cone follows statements through theorems and bodies through definitions (Harper's theorem: 9 declarations instead of its 540-node proof cone). - Generator (schema 1.2): statement/body boundary positions, module context-command tables with same-project import closure (notation-only modules included), mutual-block spans, generated-declaration hosts, and `open/set_option/attribute/variable … in` prefix reattachment. - Builder (static/assets/minimal.js, shared verbatim with a node harness): module replay in import order, namespace-aware pruning of variable/attribute/export contexts referencing out-of-cone declarations, non-builtin attribute stripping, and a tactic-reference closure pulling in `simp only [...]`-cited lemmas invisible to term-level extraction. - Validated by actually compiling generated files against Mathlib oleans across 6 harness rounds on 20 real targets spanning 14 projects (0/20 -> 13/20; the rest are documented structural limits: elaboration- consumed instances, tactic-state-sensitive definition bodies, and custom notation inside binder types). - Declarations viewer: kind filter chips now show counts for the selected project + search subset instead of pool-wide totals. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🛑 not_a_fit |
| Level | undergraduate |
| Branch | exposition tooling |
| Mode | mixed |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is repository tooling for extracting dependency cones into minimal Lean files, not a mathematical formalization.
Tokens: 21,262 in / 726 out · Tier: flex · Cost: $0.0640
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Vilin97
added a commit
that referenced
this pull request
Jul 29, 2026
#293) An audit of all 148 reviews the bot has posted, against what actually happened to those PRs, says the project review was looking in the wrong place. **It approved a duplicate.** #275 (de Bruijn-Erdos compactness) came back `approve` / `good_fit` / 0 findings and was closed by hand: the headline follows in a few lines from Mathlib's `Finsubgraph`. #225 was likewise subsumed by the pool's own `Incompleteness`. REVIEW_RULES.md never had a duplication check — only the challenge rules did. **It could not see what the axiom gate misses.** #225's diagonal lemma was postulated as an `inductive` constructor, invisible to `#print axioms`; the review filed it as a card-wording nit. Same class: #215 (a rescaled surrogate tableau proved in place of the real one), #240 (a card informal that was false), #265 (a synthetic residue model presented as the geometry it models), #199 (NP-hardness claimed for a reduction-correctness result). **Infra PRs were graded for mathematical fit.** A .lean file under scripts/ clears the workflow's "touches Lean?" filter, so the exposition PRs landed on the project rules: #279 and #282 came back `not_a_fit`/`undergraduate`, #283 came back `good_fit`/`graduate`/`approve` over a summary opening "This is not a mathematics contribution." All three merged. So the project rules gain the four checks the challenge rules already had, adapted for finished proofs — claim-vs-Lean faithfulness, what is assumed rather than proved, prior art, and source fidelity — plus the generated-bulk criterion #278 was closed on after a 0-finding approval, and an AI-slop list. Tau Ceti and ArkLib converge on the same shape. Calibration fixes from the same audit: `obscure_problem` was `no` in all 147 project reviews and is gone; card metadata moves to out-of-scope (#216 and #243 were rejected on nothing else, then merged unchanged); a partial review may no longer `approve`, since code_quality cannot be scored on elided files; and the comment now says `request_changes` is an ask, not a close — 39% of those verdicts were merged after a human looked. Two of the four approve examples (sphere packing, Erdos 124) were not in the pool at all. The reviewer also now receives the PR title and description, which the rules have always allowed to carry the source anchor. Both are contributor-written, as is the diff, so they are fenced with a per-request random token and framed as claims to verify rather than instructions. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
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.
Two follow-ups to the exposition site (#279):
Minimal Lean file (LML-style, built for the pool's scale)
Every declaration panel now has a Minimal Lean file button next to "Dependency cone": a standalone
.leanfile containing just the declaration's statement cone — definitions keep their bodies, theorem proofs are replaced bysorry— with one-click Open in Lean playground (LZ-compressed#codez=link, byte-verified against lean4web's decoder), plus download/copy. Statement-only dependency tracking keeps files small where it matters: Harper's theorem yields a 9-declaration file although its full proof cone has 540 nodes; Gödel I assembles 337 declarations from 183 modules and still fits a playground link.Unlike LML (which pregenerates one file per declaration server-side), assembly is client-side: per-project shards carry statement boundaries, statement-only deps, module context-command tables (closed over same-project imports so notation-only files replay too), mutual spans, generated-declaration hosts, and
… in-prefix reattachments; the builder fetches raw sources pinned to the shard's commit and replays each module — contexts, prunedvariable/attribute/exportcommands (namespace-aware, out-of-cone references dropped), sanitized attributes, and a tactic-reference closure that pulls insimp only [...]-cited lemmas invisible to term-level dependency extraction. No pregenerated artifacts, no site-size impact.Verification: the builder is a pure module (
minimal.js) shared verbatim between the browser and a node harness that compiled generated files against Mathlib oleans across 6 rounds on 20 real targets from 14 projects (private decls, structures, instances, mutual blocks, notation-heavy Incompleteness/PhaseRetrieval/LeanModularForms, 130+-declaration stress cones). Trajectory 0/20 → 13/20, with every remaining failure characterized and accepted: elaboration-consumed instances (CoeFun-style, invisible to term-level deps), tactic-state-sensitive definition bodies, and custom notation inside binder types. The generated file header notes it may need minor adjustments.Declarations viewer facets
Selecting a project (or typing a search) now updates the kind chips to show counts for that subset — e.g. ABCExceptions shows
lemma 120 · theorem 74 · def 37 · structure 2 · class 1 · instance 1instead of pool-wide totals.Schema additions are documented in
SCHEMA.md(§1.2). 182 pytest tests green (7 new), ruff clean, all JS syntax-checked; harness artifacts (all rounds' generated files + compile logs) preserved for the record.🤖 Generated with Claude Code