Automatic theorem classification across Lean 4 projects
Classification based on E.J. Lowe's metaphysical framework across all analyzed projects.
| Mathematical (Prop) | Computational (Data) | |
|---|---|---|
| Substantial (Types) | 7 (87%) | 1 (12%) |
| Non-substantial (Defs) | 18 (35%) | 33 (64%) |
Classification of theorems by what they prove across all analyzed projects.
| Theorem Kind | Count | Percentage |
|---|---|---|
| mathematicalProperty | 3 | 7% |
| bridgingProperty | 0 | 0% |
| computationalProperty | 0 | 0% |
| soundnessProperty | 0 | 0% |
| completenessProperty | 0 | 0% |
| unclassified | 38 | 92% |
| Project | Defs | Defs⚠️ | Thms | Thms⚠️ | Bridge | Unclass |
|---|---|---|---|---|---|---|
| LeanLangur | 1 | 0 | 0 | 0 | 0 | 0 |
| verbose-lean4 | 0 | 0 | 0 | 0 | 0 | 0 |
| proofs_with_lean | 50 | 0 | 41 | 0 | 0 | 38 |
| TOTAL | 51 | 0 | 41 | 0 | 0 | 38 |
These projects failed in the latest run but have documentation from a previous successful build.
| Project | Math Abstractions | Comp Datatypes | Math Definitions | Comp Operations |
|---|---|---|---|---|
| LeanLangur | 0 | 0 | 0 | 1 |
| verbose-lean4 | 0 | 0 | 0 | 0 |
| proofs_with_lean | 7 | 1 | 18 | 32 |
| TOTAL | 7 | 1 | 18 | 33 |
| Project | Math | Bridge | Comp | Sound | Complete | Unclass |
|---|---|---|---|---|---|---|
| LeanLangur | 0 | 0 | 0 | 0 | 0 | 0 |
| verbose-lean4 | 0 | 0 | 0 | 0 | 0 | 0 |
| proofs_with_lean | 3 | 0 | 0 | 0 | 0 | 38 |
| TOTAL | 3 | 0 | 0 | 0 | 0 | 38 |
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.