doc-verification-bridge Experiment Results

📊 Four-Category Ontology (Aggregate)

Classification based on E.J. Lowe's metaphysical framework across all analyzed projects.

	Mathematical (Prop)	Computational (Data)
Substantial (Types)	0 (0%)	249 (100%)
Non-substantial (Defs)	251 (6%)	3896 (93%)

📈 Theorem Taxonomy (Aggregate)

Classification of theorems by what they prove across all analyzed projects.

Theorem Kind	Count	Percentage
mathematicalProperty	8375	82%
bridgingProperty	4	0%
computationalProperty	0	0%
soundnessProperty	0	0%
completenessProperty	0	0%
unclassified	1716	16%

✅ Successful Projects (7)

Overview

Project	Defs	Defs⚠️	Thms	Thms⚠️	Bridge	Unclass
LeanLangur	1	0	0	0	0	0
verbose-lean4	0	0	0	0	0	0
MRiscX	269	0	116	0	1	20
cslib	767	0	1271	0	3	93
⚠️ ClassFieldTheory	289	2	966	11	0	311
⚠️ PhysLean	2432	5	5865	4	0	411
⚠️ PrimeNumberTheoremAnd	389	1	1877	208	0	881
TOTAL	4147	8	10095	223	4	1716

📚 Previously Successful Projects (10)

These projects failed in the latest run but have documentation from a previous successful build.

plausible (backup from 2026-04-03T03:17:18-07:00)
https://github.com/leanprover-community/plausible | View Previous Docs
mathlib4 (backup from 2026-04-02T03:22:56-07:00)
https://github.com/leanprover-community/mathlib4 | View Previous Docs
aesop (backup from 2026-04-03T03:17:18-07:00)
https://github.com/leanprover-community/aesop | View Previous Docs
batteries (backup from 2026-04-02T03:22:55-07:00)
https://github.com/leanprover-community/batteries | View Previous Docs
Sudoku4 (backup from 2026-03-09T22:03:40-07:00)
https://github.com/kckennylau/Sudoku4 | View Previous Docs
proofs_with_lean (backup from 2026-04-01T03:26:15-07:00)
https://github.com/PatrickMassot/proofs_with_lean | View Previous Docs
SDG (backup from 2026-02-22T02:58:22-08:00)
https://github.com/riccardobrasca/SDG | View Previous Docs
FLT (backup from 2026-02-06T02:56:06-08:00)
https://github.com/ImperialCollegeLondon/FLT | View Previous Docs
Hochster (backup from 2026-02-17T03:24:18-08:00)
https://github.com/FMLJohn/Hochster | View Previous Docs
banach-tarski (backup from 2026-02-17T02:56:00-08:00)
https://github.com/aetilley/banach-tarski | View Previous Docs

✅ Successful Projects — Details

Four-Category Ontology per Project

Project	Comp Datatypes	Math Definitions	Comp Operations
LeanLangur	0	0	1
verbose-lean4	0	0	0
MRiscX	5	4	265
cslib	106	98	669
ClassFieldTheory	11	0	289
PhysLean	113	112	2320
PrimeNumberTheoremAnd	14	37	352
TOTAL	249	251	3896

Theorem Taxonomy per Project

Project	Math	Bridge	Unclass
LeanLangur	0	0	0
verbose-lean4	0	0	0
MRiscX	95	1	20
cslib	1175	3	93
ClassFieldTheory	655	0	311
PhysLean	5454	0	411
PrimeNumberTheoremAnd	996	0	881
TOTAL	8375	4	1716

❌ Failed Projects (23)

mm0 — Toolchain incompatibility: project uses leanprover/lean4:v4.13.0, supported range is v4.24.0 to v4.29.0
https://github.com/digama0/mm0 | View Details
plausible — Toolchain incompatibility: project uses leanprover/lean4:v4.30.0-rc1, supported range is v4.24.0 to v4.29.0
https://github.com/leanprover-community/plausible | View Details
mathlib4 — Toolchain incompatibility: project uses leanprover/lean4:v4.30.0-rc1, supported range is v4.24.0 to v4.29.0
https://github.com/leanprover-community/mathlib4 | View Details
aesop — Toolchain incompatibility: project uses leanprover/lean4:v4.30.0-rc1, supported range is v4.24.0 to v4.29.0
https://github.com/leanprover-community/aesop | View Details
batteries — Toolchain incompatibility: project uses leanprover/lean4:v4.30.0-rc1, supported range is v4.24.0 to v4.29.0
https://github.com/leanprover-community/batteries | View Details
logical_verification_2025 — Toolchain incompatibility: project uses leanprover/lean4:v4.14.0, supported range is v4.24.0 to v4.29.0
https://github.com/lean-forward/logical_verification_2025 | View Details
lean-loris — Toolchain incompatibility: project uses leanprover/lean4:v4.7.0, supported range is v4.24.0 to v4.29.0
https://github.com/siddhartha-gadgil/lean-loris | View Details
RLTL-derivatives — Toolchain incompatibility: project uses leanprover/lean4:v4.7.0, supported range is v4.24.0 to v4.29.0
https://github.com/ezhuchko/RLTL-derivatives | View Details
puzzles — Build failed
https://github.com/arademaker/puzzles | View Details
LeanLion — Toolchain incompatibility: project uses leanprover/lean4:v4.22.0, supported range is v4.24.0 to v4.29.0
https://github.com/siddhartha-gadgil/LeanLion | View Details
Polylean — Toolchain incompatibility: project uses leanprover/lean4:v4.19.0-rc3, supported range is v4.24.0 to v4.29.0
https://github.com/siddhartha-gadgil/Polylean | View Details
fil-rb — Toolchain incompatibility: project uses leanprover/lean4:v4.15.0-rc1, supported range is v4.24.0 to v4.29.0
https://github.com/hargoniX/fil-rb | View Details
SciLean — Build failed
https://github.com/lecopivo/SciLean | View Details
LeanMetaCompute — Build failed
https://github.com/siddhartha-gadgil/LeanMetaCompute | View Details
fad — Build failed
https://github.com/arademaker/fad | View Details
Sudoku4 — lake update failed
https://github.com/kckennylau/Sudoku4 | View Details
proofs_with_lean — Build failed
https://github.com/PatrickMassot/proofs_with_lean | View Details
EllipticCurve — lake update failed
https://github.com/kckennylau/EllipticCurve | View Details
SDG — lake update failed
https://github.com/riccardobrasca/SDG | View Details
FLT — Build failed
https://github.com/ImperialCollegeLondon/FLT | View Details
Hochster — Build failed
https://github.com/FMLJohn/Hochster | View Details
banach-tarski — Build failed
https://github.com/aetilley/banach-tarski | View Details
MCMC — Build failed
https://github.com/or4nge19/MCMC | View Details

📋 Configuration

View the config.toml file used for analyzing these projects.

📝 Want to add a project? Submit a PR to suggest additional Lean 4 projects for analysis.

🔬 doc-verification-bridge Experiment Results