Lean formalizations, verified correspondences, and open reading points. Every story connects its mathematical statement to the code and evidence behind it.
Featured verification
Latest result
OpenAI Math 378 · Complexity theory
A verified negation of PositiveRateETH
Lean 4.34.1 derives ¬ PositiveRateETH from OpenAI’s bounded-width SAT theorem (at width 3), through an exact encoding converter and polynomial-overhead machine simulation.
● Kernel-checked11,600 build jobs · exit 03 reading points