Import optimized Infinitary Logic formalization - #399
Open
Vilin97 wants to merge 8 commits into
Open
Conversation
|
Too many files changed for review (200 files, 100 file limit). Bypass the limit by tagging |
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: 25,127 maxHeartbeats units across 198 files (44,334 added LOC). Sum of Count-heartbeats wall-clock total: 444.61 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.InfinitaryLogic.Methods.SchemaTermTruth |
37.00 s |
LeanPool.InfinitaryLogic.Descriptive.Mycielski |
15.00 s |
LeanPool.InfinitaryLogic.Descriptive.GSGraph |
14.00 s |
LeanPool.InfinitaryLogic.Util |
10.00 s |
LeanPool.InfinitaryLogic.Methods.SchemaLocalEMSource |
9.40 s |
LeanPool.InfinitaryLogic.Descriptive.KuratowskiUlam |
9.10 s |
LeanPool.InfinitaryLogic.Methods.Interpolation.BudgetedPair |
8.70 s |
LeanPool.InfinitaryLogic.Mathlib.ModelTheory.Infinitary.Syntax |
7.10 s |
LeanPool.InfinitaryLogic.Methods.Interpolation.PairedInsepFamily |
5.80 s |
LeanPool.InfinitaryLogic.Methods.Henkin.CountableCompletion.GeneratedUniverse |
5.60 s |
LeanPool.InfinitaryLogic.Methods.SchemaCompletion |
5.20 s |
LeanPool.InfinitaryLogic.Methods.WellOrdering.ClosureFields |
5.20 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 198 files; the per-file table shows only the 198 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.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | 🤔 discuss |
Based on the partial diff, faithfulness is unverifiable because the project card and several headline declaration signatures are omitted. |
| Novelty | ✅ pass |
Based on the partial diff, none of the eight searched headline results is already formalized in Mathlib or the listed pool projects. |
| Significance | ✅ pass |
Based on the partial diff, this is a good-fit research-level theory-building project with several major named results in infinitary model theory and descriptive set theory. |
| Sources | 🤔 discuss |
Based on the partial diff, the citations are otherwise internally consistent, but the López–Escobar locator for the Lyndon polarity claim must be resolved. |
| Code quality (advisory) | 🤔 discuss |
Based on the partial diff, the visible Lean is competent, but unused public assumptions, duplicated separation plumbing, and post-DCE scaffolding and import residue need a maintainer pass. |
| Aspect | Value |
|---|---|
| Proves the claim | ➖ unverifiable |
| Assumed, not proved | Visible headlines assume, among other inputs, countable symbol types and a ConsistencyPropertyEq L for model_existence, relationality and a universal consequent for malitz_interpolation, HasWellOrderedChains φ lt for exists_model_relPreserving, a uniform well-order hypothesis for wellOrder_type_boundedness, bounded Scott height for iso_borel_of_bounded_scottHeight, and finite satisfiability inside finitaryFragment L for finitaryFragment_compact; whether the card discloses these inputs is unavailable. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | infinitary model theory and descriptive set theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: Visible endpoints include unconditional results such as morley_hanf and conditional results such as model_existence, malitz_interpolation, and finitaryFragment_compact, but their exact card informals cannot be compared with the Lean.
The visible Lean develops a substantial infinitary-logic theory culminating in Karp, Craig, Lyndon, Malitz, López–Escobar, Silver–Burgess, Morley–Hanf, exact Hanf-number, small-model, and well-order non-Borelness theorems.
Faithfulness findings (1)
- partial-diff-unverifiable — PR-wide
Theprojects.ymlcard content is omitted, so none of the 31 declaration/informal pairs can be audited. Several headline-bearing files are also omitted, including the Scott sentence/rank and Morley counting endpoints. Provide the card and all headline signatures in the review artifact.
Evidence: The visible conditional signatures includetheorem model_existence [Countable (Σ l, L.Functions l)] [_countableRelations : Countable (Σ l, L.Relations l)] (C : ConsistencyPropertyEq L) (S : Set L.Sentenceω) (hS : S ∈ C.toConsistencyProperty.sets) (_hS_countable : S.Countable) :andtheorem malitz_interpolation [L.IsRelational] (φ ψ : L.Sentenceω) (hψ : IsUniversal ψ) (h : Sentenceω.Entails φ ψ) :; the corresponding card informals are not present in the diff.
Sources findings (1)
- source-mismatch —
LeanPool/InfinitaryLogic/Methods/Interpolation/LyndonInseparability.lean:34
The same Lyndon polarity claim is assigned two different theorem numbers. The cited paper is not included, so the diff does not establish whether 4.0(.4) or 4.1 is correct; verify the source and normalize the locator across the Lyndon files.
Evidence:LyndonArbitrary.leancalls thisThe relation-polarity / logical-equality form of López–Escobar 1965, Theorem 4.1 (clause (.4) in full; clause (.3)'s equality-occurrence condition is not claimed), while this file saysThis is the machine-checked form of the side flip in López–Escobar 1965, Theorem 4.0(.4).
Code quality findings (4)
- unused-hypothesis — PR-wide
Several public declarations retain assumptions that their proofs do not consume. Remove them from the minimal theorem statements; if source-signature compatibility is required, keep compatibility wrappers around stronger assumption-free declarations.
Evidence:encodeViaEquiv_modelsdeclares[_countableα : Countable α], but its proof isby rw [toStructure_encodeViaEquiv_eq] let : L.Structure α := Equiv.inducedStructure e exact (LomegaEquiv.of_equiv (Equiv.inducedStructureEquiv e) φ).mp hφ.model_existencedeclares(_hS_countable : S.Countable)but ends withexact ⟨TermModel C S' hmax, termModelStructure, inferInstance, fun φ hφ => (truthLemma φ).mp (hSS' hφ)⟩.stabilization_bound_iso_eq_BFEquivdeclares(_hα : α < Ordinal.omega 1), andbounded_scottHeight_iso_eq_BFEquivdeclares(_hN : Sentenceω.Realize φ N)while its body isbounded_scottHeight_iso_eq_BFEquiv_of countableRefinementHypothesis hα hbound hM.graphExpansion_realizes_pcSentencelikewise declares[_nonemptyM : Nonempty M]without using it. - duplicate-implementation —
LeanPool/InfinitaryLogic/Methods/Interpolation/CraigArbitrary.lean:138
craig_pcSeparationduplicates the restriction and semantic-transport proof incraig_pcSeparation_relational; only the interpolation theorem invoked at the start differs. Factor the shared conversion from a Craig interpolant witness to the shared-sublanguage separator, or make the relational theorem a wrapper around the arbitrary-language theorem.
Evidence: The arbitrary proof startsobtain ⟨θ, hθF, hθR, hE1, hE2⟩ := craig_interpolation ψ₁ ψ₂.not hand then repeatsrw [BoundedFormulaω.functionsIn_not] at hθF,rw [BoundedFormulaω.relationsIn_not] at hθR, the definitions ofF₀andR₀, bothrealize_mapLanguagetransports, and the final negation argument.craig_pcSeparation_relationalhas the same body beginningobtain ⟨θ, hθF, hθR, hE1, hE2⟩ := craig_interpolation_relational ψ₁ ψ₂.not h. - agent-slop — PR-wide
The declaration-level DCE left empty section scaffolding in multiple modules. These banners describe APIs that are no longer present and obscure the actual retained surface; remove the empty sections and trim the surrounding historical module commentary.
Evidence:LeanPool/InfinitaryLogic/Descriptive/LopezEscobar.leanends its namespace immediately after/-! ## The collection equality (issue #28, target 7) -/.LeanPool/InfinitaryLogic/Methods/SkolemClosure.leanends with the consecutive empty blocks/-! ### Staged formulas and the colimit projection -/,/-! ### Existential Skolem-witness step (stagek→k+1) -/,/-! ### The Skolem-closed staged familyΓ*-/, and/-! ### Colimit image and enumeration -/. - unused-import —
LeanPool/InfinitaryLogic/Descriptive/CountingDichotomy.lean:7
The visible file only defines the abstractSilverBurgessDichotomyproposition, so the direct imports ofIsomorphismBorelandStructureIsoSetoidare residue from the removed counting theorem. Replace them with the minimal imports needed forStandardBorelSpace,MeasurableSet, and cardinal continuum.
Evidence: The file importsLeanPool.InfinitaryLogic.Descriptive.IsomorphismBorelandLeanPool.InfinitaryLogic.Descriptive.StructureIsoSetoid, but its only declaration isdef SilverBurgessDichotomy : Prop := ∀ {X : Type w} [MeasurableSpace X] [StandardBorelSpace X] (r : Setoid X), MeasurableSet {p : X × X | r.r p.1 p.2} → (#(Quotient r) ≤ ℵ₀) ∨ (#(Quotient r) = Cardinal.continuum).
Tokens: 2,725,536 in / 25,800 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $14.2082
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.
Owner
Author
|
Addressed the actionable automated-review findings in
The López–Escobar references are intentionally different, not inconsistent. The pinned source's frozen Lyndon audit distinguishes Theorem 4.1's formula-form endpoint from Theorem 4.0's sequent-form orientation check; Local evidence for the new head:
The PR body now carries the corrected final LOC, closure, public-audit, and direct-import counts. Fresh exhaustive lint/axiom checks are running in CI. |
# Conflicts: # LeanPool/projects.yml
Owner
Author
Automation disposition: needs-maintainerReviewed exact head |
Vilin97
added
the
needs-maintainer
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
1 participant
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.
Summary
Imports the proved headline surface of Cameron Freer's Infinitary Logic in Lean 4: Scott sentences and ranks, Karp's theorem, model existence and the sharp Morley--Hanf bound, Craig/Lyndon/Malitz interpolation, López--Escobar definability and well-order non-Borelness, Silver--Burgess/Morley counting, and honest HF compactness.
The source is pinned at
4d0c43c5288952267e7d5478d79302cae17945a9under Apache-2.0. Four necessary infinitary-syntax compatibility leaves descend from the source's Mathlib fork at4038001c613926e4d3f3791977380be96a19c192, also under Apache-2.0. Proof provenance is recorded honestly asmixbecause the import retains Cameron Freer's proofs while substantially refactoring and minimizing them here.This deliberately does not mirror the source's broad
InfinitaryLogic.Allfacade. Exact theorem-root closure excludes off-path/WIP/historical material, including the conditionalAdmissible/Barwise/*,Admissible/Compactness, andAdmissible/Nadelscaffolding. The retainedAdmissiblesurface is the proved family/honest-HF interface.Exact headline roots
The import and audits are rooted at these 31 declarations:
FirstOrder.Language.scottSentenceFirstOrder.Language.scottSentence_characterizesFirstOrder.Language.scottRankFirstOrder.Language.scottRank_lt_omega1FirstOrder.Language.karp_theorem_wFirstOrder.Language.model_existenceFirstOrder.Language.morley_hanfFirstOrder.Language.Lomega1omegaHanfNumber_eq_beth_omega1FirstOrder.Language.exists_small_model_of_hasArbLargeModelsFirstOrder.Language.exists_complete_sentence_of_lomega1omegaSmallFirstOrder.Language.exists_complete_kCategorical_of_hasArbLargeModelsFirstOrder.Language.craig_interpolationFirstOrder.Language.craig_pcSeparationFirstOrder.Language.lyndon_interpolationFirstOrder.Language.malitz_interpolationFirstOrder.Language.exists_model_relPreservingFirstOrder.Language.wellOrder_type_boundednessFirstOrder.Language.wellOrdering_undefinableFirstOrder.Language.lopezEscobar_iffFirstOrder.Language.lopezEscobar_action_iffFirstOrder.Language.wellOrderClass_not_measurableSetgandy_harrington_for_relationFirstOrder.Language.silverBurgessDichotomyFirstOrder.Language.morley_countingFirstOrder.Language.iso_borel_of_bounded_scottHeightFirstOrder.Language.FamilyPresentationFirstOrder.Language.CodedFamilyFirstOrder.Language.AdmissibleFragmentFirstOrder.Language.hfFragmentFirstOrder.Language.hfAdmissibleFragmentFirstOrder.Language.finitaryFragment_compactClosure and source reduction
All counts below were recomputed from the pinned source and the final compiled environment.
Allclosure376 + 422 = 798declaration commands, with zero restorations.private; every downstream endpoint was rebuilt after the batches.Allclosure, the final tree retains 59 fewer modules and 17,804 fewer physical lines (28.9%).set_optioncommands were eliminated. Warning cleanup went from 621 initial build warnings (540 after DCE) to zero, without waivers.The narrow entry imports only 21 endpoint-bearing leaves. Excluding that facade, direct import edges fell from 498 to 484: internal project edges fell from 395 to 370, while exact Mathlib leaf edges rose from 103 to 114 as internal facades were replaced by precise direct imports; distinct Mathlib leaves are 69. Lake's project job closure fell from 2,134 to 2,117.
Reuse audit
ModelTheory/Infinitarydirectory and no compatibleBoundedFormulaInf,FormulaInf,SentenceInf, carrier transport, orIndexCodingpackage.Syntax,Semantics,IndexCoding, andReindextherefore remain as minimized compatibility leaves. The five source leaves totaled 1,068 lines; the retained four total 571 lines.QuantifierRankand all consumers were outside exact endpoint closure, so that leaf was deleted completely (497 transformed lines; 238 lines in the pinned fork source).LeanPool.LeanQuantumAlgfound no compatible abstractions to reuse; its quantum-algorithm vocabulary does not match this model-theoretic syntax/semantics layer, so no adapter was forced.Contract audit
All 31 endpoint types were independently compared with the pinned source and all endpoint axiom sets were rechecked. Contract-neutral linter repairs rename
Formulaω.realize_as_sentencetorealizeAsSentenceand underscore a few unused binder names. After normalizing only those spellings, the source and final signature bundles have the identical SHA-256516ffb216ef3c9245f1aa6aa80938dea156d037795199096ebb87f9c61eec3bb; dedicated Lean restatements prove the pretty-printed differences definitionally equal. Final endpoint axiom output is byte-identical to the pre-golf audit and uses onlypropext,Classical.choice, andQuot.sound(several endpoints use fewer or none).Verification and measured cost
lake build LeanPool.InfinitaryLogicat the same 2,117-job closure: 62.24 s wall, 2,444,356 KB peak RSS, warning-free.LeanPool.leancollision compile, using current-worktree project artifacts and only seeded missing base submodule artifacts (never a borrowed top-levelLeanPool.olean): passed. First seeded run: 32.48 s / 7,487,824 KB; final warm recheck after the cold project build: 4.53 s / 7,536,408 KB.lake exe runLinter --no-build LeanPool: all 14 linters passed (40.45 s / 9,372,900 KB).lake exe lint-style LeanPool: passed (3.24 s / 861,328 KB).python -m lean_pool.quality --repo ..: passed, including forbidden-token, option-backdoor, header, file/proof-size, registry, and all-public-declaration axiom gates (7:02.42 / 11,519,868 KB).lake exe mk_all --check: passed.git diff --check, and content-only path audit: passed.e690cb14: warning-free 2,117-job project build, explicit style check over all 197 submodules, static quality, refreshed kernel/source closures, andgit diff --check: passed. Fresh exhaustive linter and axiom checks are delegated to CI.