asagolf
Objective-C++
★ 1
updated 2mo ago
Exact ZFC-grounded proof size of a Birkhoff triangle-congruence theorem: a micro-kernel Metamath verifier + kernel-checked proof objects. Geometry is ~10^7; the 10^1000 estimate is off by ~950 OOM.
No plain-English explanation yet — one is being written right now. Check back in a minute.