Repository navigation
Add formal learning theory kernel - #28
Merged
Merged
Conversation
There was a problem hiding this comment.
Pull request overview
This PR ports the formal-learning-theory kernel (from merely-true#36) into Lean Pool as LeanPool.FormalLearningTheory, adding a substantial Lean development around PAC/Gold/online learning criteria, complexity measures (VC/Littlestone/mind-change/ordinal extensions), and supporting measure-theoretic/descriptive-set-theoretic infrastructure; it also updates the Python “quality” tooling to correctly parse Lean declaration names ending in prime (') and adds a regression test.
Fit: good_fit
Level: research
Branch: formal learning theory / descriptive set theory / probability
Mode: theory_building
Obscure problem: false
Code quality: 3/5
Significance: Introduces a broad, reusable kernel for formal learning theory (definitions + major structural theorems), plus tooling needed to keep the new Lean surface area CI-auditable.
Verdict: request_changes
Findings:
splitFirst/splitSeconddo not useValidSplitand therefore do not implement the intended split-by-assignment semantics (critical correctness issue).- A knowingly incorrect “branch-wise” shattering predicate is exported under the generic name
MistakeTree.isShattered, increasing risk of downstream misuse.
Changes:
- Add
LeanPool.FormalLearningTheorykernel: core types, learning criteria, complexity measures, and key theorems (e.g., Gold/mind-change characterization) plus pure-math support modules. - Extend Python quality checker regexes to preserve prime-suffixed Lean names and relax axiom-audit output parsing accordingly.
- Add a regression test ensuring the quality checker parses prime-suffixed declarations.
Reviewed changes
Copilot reviewed 56 out of 59 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| python/tests/test_quality.py | Adds regression test for parsing declarations ending in '. |
| python/lean_pool/quality.py | Fixes declaration/axiom-output parsing to preserve prime suffixes. |
| LeanPool/FormalLearningTheory/Theorem/Gold.lean | Adds Gold’s theorem proof and mind-change characterization theorem. |
| LeanPool/FormalLearningTheory/Theorem.lean | New theorem index for the learning theory module. |
| LeanPool/FormalLearningTheory/PureMath/ReaderMonad.lean | Adds a pure Reader-selection monad used for learner composition. |
| LeanPool/FormalLearningTheory/PureMath/KLDivergence.lean | Introduces finite-PMF infrastructure and KL/cross-entropy/expectation defs. |
| LeanPool/FormalLearningTheory/PureMath/FiniteVCApprox.lean | Adds finite-distribution approximation lemmas (TV → test expectation bounds). |
| LeanPool/FormalLearningTheory/PureMath/Exchangeability.lean | Adds exchangeability/double-sample infrastructure (merged samples, splits, split measure). |
| LeanPool/FormalLearningTheory/PureMath/Concentration.lean | Adds concentration inequality infrastructure (Chebyshev-majority bound). |
| LeanPool/FormalLearningTheory/PureMath/BinaryMatrix.lean | Adds binary-matrix VC dimension + Sauer–Shelah + dual VC bound infrastructure. |
| LeanPool/FormalLearningTheory/PureMath/AnalyticMeasurability.lean | Adds analytic→null-measurable bridge via Choquet capacity arguments. |
| LeanPool/FormalLearningTheory/Process.lean | Adds process-level/application-layer structures and markers (grammar induction, CEGIS, etc.). |
| LeanPool/FormalLearningTheory/Learner/VersionSpace.lean | Adds version-space learner and measurability proof via countable decomposition. |
| LeanPool/FormalLearningTheory/Learner/Properties.lean | Adds learner property predicates and a helper lemma for MeasurableBatchLearner. |
| LeanPool/FormalLearningTheory/Learner/Monad.lean | Adds measurable learner monad wrapper and evaluation-level monad laws. |
| LeanPool/FormalLearningTheory/Learner/Core.lean | Defines core learner types and MeasurableBatchLearner regularity class. |
| LeanPool/FormalLearningTheory/Learner/Closure.lean | Proves closure of measurable learners under combiners/boosting/selection. |
| LeanPool/FormalLearningTheory/Learner/Bayesian.lean | Adds Bayesian learner/inference structures and a Gibbs posterior wrapper. |
| LeanPool/FormalLearningTheory/Learner/Active.lean | Adds active learning/teacher/meta-learning interfaces and related predicates. |
| LeanPool/FormalLearningTheory/Learner.lean | New learner index module. |
| LeanPool/FormalLearningTheory/Data.lean | Adds data/presentation interfaces (streams, texts, IID samples, oracles). |
| LeanPool/FormalLearningTheory/Criterion/PAC.lean | Defines PAC/agnostic PAC/exact learning criteria. |
| LeanPool/FormalLearningTheory/Criterion/Online.lean | Defines online criteria and helpers (mistakes/loss/regret). |
| LeanPool/FormalLearningTheory/Criterion/Gold.lean | Defines Gold-style success criteria (EX/BC/etc.) and dataUpTo. |
| LeanPool/FormalLearningTheory/Criterion/Extended.lean | Adds cross-paradigm/extended criteria (drift, universal learning, advice, Bayesian). |
| LeanPool/FormalLearningTheory/Criterion.lean | New criteria index module. |
| LeanPool/FormalLearningTheory/Computation.lean | Adds computability/formal-language substrate and information-theoretic primitives. |
| LeanPool/FormalLearningTheory/Complexity/VCDimension.lean | Adds core VC dimension/shattering/growth/star-number definitions. |
| LeanPool/FormalLearningTheory/Complexity/Structures.lean | Adds structured complexity notions (compression, multiclass dims, SQ, etc.). |
| LeanPool/FormalLearningTheory/Complexity/Ordinal.lean | Adds ordinal-valued extensions and embedding lemmas. |
| LeanPool/FormalLearningTheory/Complexity/MindChange.lean | Adds mind-change count/ordinal definitions for Gold learners. |
| LeanPool/FormalLearningTheory/Complexity/Littlestone.lean | Adds a branch-wise Littlestone infrastructure and helper lemmas. |
| LeanPool/FormalLearningTheory/Complexity/Interpolation.lean | Adds interpolation constructions and well-behavedness descent results. |
| LeanPool/FormalLearningTheory/Complexity/Generalization.lean | Adds an index module for generalization infrastructure. |
| LeanPool/FormalLearningTheory/Complexity/GameInfra.lean | Adds corrected depth-indexed Littlestone trees + SOA/game infrastructure. |
| LeanPool/FormalLearningTheory/Complexity/DualVC.lean | Adds dual-class construction and Assouad-style dual VC bound. |
| LeanPool/FormalLearningTheory/Complexity/BorelAnalyticBridge.lean | Adds Borel→analytic→null-measurable bridge for learning-theory bad events. |
| LeanPool/FormalLearningTheory/Complexity/Amalgamation.lean | Adds amalgamation construction and well-behavedness result. |
| LeanPool/FormalLearningTheory/Complexity.lean | New complexity index module. |
| LeanPool/FormalLearningTheory/Basic.lean | Adds foundational learning-theory types (concepts, classes, loss, etc.). |
| LeanPool/FormalLearningTheory.lean | New top-level module entry for the learning theory kernel. |
| LeanPool.lean | Extends the root import surface to include the new learning theory hierarchy. |
Comment on lines
+118
to
+128
| /-- Given a merged sample z and a valid split, extract the first group (training sample). -/ | ||
| def splitFirst {X : Type u} {m : ℕ} (z : MergedSample X m) (_vs : ValidSplit m) : | ||
| Fin m → X := by | ||
| -- The first group consists of the m indices where assign = true | ||
| -- We need to enumerate them and index into z | ||
| exact fun i => z (Fin.castAdd m i |>.cast (two_mul m).symm) | ||
|
|
||
| /-- Given a merged sample z and a valid split, extract the second group (ghost sample). -/ | ||
| def splitSecond {X : Type u} {m : ℕ} (z : MergedSample X m) (_vs : ValidSplit m) : | ||
| Fin m → X := by | ||
| exact fun i => z (Fin.natAdd m i |>.cast (two_mul m).symm) |
Comment on lines
+36
to
+53
| The correct definition (used in `Theorem/Online.lean`) restricts C at each branch: | ||
| | .branch x l r => | ||
| (∃ c ∈ C, c x = true) ∧ (∃ c ∈ C, c x = false) ∧ | ||
| isShattered X {c ∈ C | c x = true} l ∧ | ||
| isShattered X {c ∈ C | c x = false} r | ||
|
|
||
| The characterization theorem uses the corrected version. -/ | ||
| def MistakeTree.isShattered (X : Type u) (C : ConceptClass X Bool) : | ||
| MistakeTree X → Prop | ||
| | .leaf => True | ||
| | .branch x l r => | ||
| (∃ c ∈ C, c x = true ∧ MistakeTree.isShattered X C l) ∧ | ||
| (∃ c ∈ C, c x = false ∧ MistakeTree.isShattered X C r) | ||
|
|
||
| /-- Littlestone dimension (branch-wise variant): see `Theorem/Online.lean` for the | ||
| corrected path-consistent version used in the characterization theorem. -/ | ||
| noncomputable def BranchWiseLittlestoneDim (X : Type u) (C : ConceptClass X Bool) : WithTop ℕ := | ||
| ⨆ (T : MistakeTree X) (_ : T.isShattered X C), (T.depth : WithTop ℕ) |
Vilin97
force-pushed
the
codex/formal-learning-theory-pr36
branch
3 times, most recently
from
May 10, 2026 01:46
52c53c7 to
a728f94
Compare
Contributor
Proof profile (new / modified Lean files)
Per-file profile output
|
Collaborator
Author
|
/review |
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | statistical learning theory |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a broad Lean kernel for formal learning theory, including the PAC/VC characterization, Littlestone online characterization, compression-with-side-information equivalence, Rademacher and measurability bridges, and paradigm separation results.
Tokens: 402,313 in / 764 out · Tier: standard · Cost: $2.0345
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Vilin97
force-pushed
the
codex/formal-learning-theory-pr36
branch
from
May 10, 2026 07:38
6c86015 to
ffbd231
Compare
Comment on lines
+118
to
+128
| /-- Given a merged sample z and a valid split, extract the first group (training sample). -/ | ||
| def splitFirst {X : Type u} {m : ℕ} (z : MergedSample X m) (_vs : ValidSplit m) : | ||
| Fin m → X := by | ||
| -- The first group consists of the m indices where assign = true | ||
| -- We need to enumerate them and index into z | ||
| exact fun i => z (Fin.castAdd m i |>.cast (two_mul m).symm) | ||
|
|
||
| /-- Given a merged sample z and a valid split, extract the second group (ghost sample). -/ | ||
| def splitSecond {X : Type u} {m : ℕ} (z : MergedSample X m) (_vs : ValidSplit m) : | ||
| Fin m → X := by | ||
| exact fun i => z (Fin.natAdd m i |>.cast (two_mul m).symm) |
Comment on lines
+37
to
+50
| /-- KL divergence between two FinitePMFs over a finite type. | ||
| KL(Q‖P) = ∑_h Q(h) · log(Q(h)/P(h)). | ||
| Convention: 0 · log(0/p) = 0. -/ | ||
| noncomputable def klDivFinitePMF {H : Type*} [Fintype H] | ||
| (Q P : FinitePMF H) : ℝ := | ||
| ∑ h : H, if Q.prob h = 0 then 0 | ||
| else Q.prob h * Real.log (Q.prob h / P.prob h) | ||
|
|
||
| /-- Cross-entropy: ∑_h Q(h) · log(1/P(h)). | ||
| Equals KL(Q‖P) + H(Q) where H(Q) is Shannon entropy. -/ | ||
| noncomputable def crossEntropyFinitePMF {H : Type*} [Fintype H] | ||
| (Q P : FinitePMF H) : ℝ := | ||
| ∑ h : H, if Q.prob h = 0 then 0 | ||
| else Q.prob h * Real.log (1 / P.prob h) |
Comment on lines
+10
to
+14
| # Measurable Batch Learner Monad | ||
|
|
||
| MeasurableBatchLearner is a measurable instance of the pure ReaderSel monad | ||
| (MathLib/ReaderMonad.lean). The algebraic structure (pure, bind, monad laws) | ||
| lives in the pure math layer. This file adds the measurability certificate. |
Collaborator
Author
|
/review |
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🟡 borderline |
| Level | research |
| Branch | statistical learning theory |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 2 / 5 |
A cleaned version would be a significant formalization of the fundamental theorem of statistical learning and related learning-theory characterizations, but the current export surface contains too many theorem names whose statements do not match their mathematical claims.
Findings (3)
- statement-mismatch — PR-wide
Several exported declarations have theorem names and surrounding prose that claim substantive learning-theory results while the Lean statement is trivial or much weaker, for examplegold_does_not_imply_pac : True, the weaksauer_shelahexistential bound, andmeta_pac_boundwithmf := 0. These should either be removed from the public project, renamed as explicit placeholders/markers, or replaced by the actual mathematical statements before merging. - project-card —
LeanPool/FormalLearningTheory.lean:10
The entry-point project card only says this is a port from a GitHub repository. It should identify the main formalized theorems intended as the project deliverables and cite the mathematical sources for them; the detailed paper references scattered through submodules do not substitute for a usable project card. - export-surface — PR-wide
The PR imports and exposes a large number of scope markers, open-question definitions, alternative interfaces, and application skeletons alongside the main theorems. For a Lean Pool project, the public surface should be trimmed to the completed formalization: keep the definitions and lemmas consumed by the main results, and move non-consuming markers or speculative future-work scaffolding out of the imported project.
Tokens: 389,765 in / 1,610 out · Tier: flex · Cost: $0.9986
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | 🟡 borderline |
| Level | research |
| Branch | statistical learning theory |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 2 / 5 |
A clean formalization of VC/PAC/Littlestone/compression/measurability theory would be significant, but this PR currently mixes substantial theorems with public placeholder and vacuous statements.
Findings (4)
- project-card-incomplete —
LeanPool/FormalLearningTheory.lean:10
The entry-point module docstring only says this is a formal learning theory kernel ported from a GitHub repository. For a project of this size it should state the main formalized theorems, the paper/textbook sources for each major component, authorship, and which parts are complete versus scaffolding or exploratory. - vacuous-public-theorem —
LeanPool/FormalLearningTheory/Complexity/Generalization/Core.lean
gold_does_not_imply_pac : Trueis not a separation theorem and should not be part of the public project API. Replace it with the actual quantified separation statement or remove it in favor of the real result in the separation file. - vacuous-public-theorem —
LeanPool/FormalLearningTheory/Theorem/Extended.lean
meta_pac_boundis explicitly noted in the proof as trivial viamf = 0; as stated it does not formalize a meta-learning bound. Remove it or strengthen the statement so the produced sample-complexity function is required to achieve PAC and the claimed comparison is mathematically meaningful. - statement-mismatch —
LeanPool/FormalLearningTheory/Theorem/PAC.lean
occam_algorithmis presented as an Occam theorem but the proof only invokes finite VC dimension and ignores the description-length content except as an unused hypothesis. Either rename it as a corollary of VC learnability or replace it with the quantitative Occam bound using the description-length assumption.
Tokens: 389,765 in / 1,943 out · Tier: flex · Cost: $1.0036
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Contributor
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | statistical learning theory |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a self-contained Lean development of the main structural equivalences and separations in formal learning theory, including named PAC/VC, compression, Gold, online, Rademacher, and measurability results.
Tokens: 386,444 in / 551 out · Tier: flex · Cost: $0.9744
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
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.
Ports merely-true/merely-true#36 into Lean Pool as LeanPool.FormalLearningTheory.
CI-oriented changes included in the port:
Local checks run on the branch: