jdhart81

jdhart81/intelligence-bound-lean

Formal verification of "The Intelligence Bound" (Hart 2025) in Lean 4 / Mathlib — 9 theorems, 0 sorry

3 good first / help-wanted issues · Lean · last activity Oct 2, 2026

0 stars 0 forks 0 watchers Lean Apache License 2.0
formal-verification information-theory lean4 mathlib theorem-proving thermodynamics
View on GitHub Website
3 Open Issues Need Help Last updated: Oct 2, 2026

Open Issues Need Help

View All on GitHub
Run `#lint` in CI and fix its 9 findings without changing statements 23 days ago
documentation enhancement help wanted good first issue
jdhart81/intelligence-bound-lean
0

Formal verification of "The Intelligence Bound" (Hart 2025) in Lean 4 / Mathlib — 9 theorems, 0 sorry

Lean
#formal-verification#information-theory#lean4#mathlib#theorem-proving#thermodynamics
Add a non-vacuity test for `intelligence_bound` and `data_wall` 23 days ago
enhancement help wanted good first issue
jdhart81/intelligence-bound-lean
0

Formal verification of "The Intelligence Bound" (Hart 2025) in Lean 4 / Mathlib — 9 theorems, 0 sorry

Lean
#formal-verification#information-theory#lean4#mathlib#theorem-proving#thermodynamics
Extend the axiom audit to all 22 theorems and lemmas 23 days ago
enhancement help wanted good first issue
jdhart81/intelligence-bound-lean
0

Formal verification of "The Intelligence Bound" (Hart 2025) in Lean 4 / Mathlib — 9 theorems, 0 sorry

Lean
#formal-verification#information-theory#lean4#mathlib#theorem-proving#thermodynamics