Back to record ledger
Kernel verified
More than two thirds on the critical line
The immutable starting record, replayed against a Mathlib-only statement with Lean Comparator.
Certified lower bound67.2500703679%
κ = 2 - 1 / cMTThe immutable starting record, replayed against a Mathlib-only statement with Lean Comparator.
κ = 2 - 1 / cMT