23,460
verified declarations
19 projects · 424K lines of Lean 4
19 projects · 424K lines of Lean 4
0 verified
265 open
98.9% complete
Gift Division
#1
jill
for Jill Campbell · gemstone optics
879 declarations
Gemstone beauty factors into two independent subspaces. Tim proved rutile beats diamond when hardness is tradeable — a result with no prior publication.
#2
audrey
Lateral curl grows as time cubed. Same contact law from granite to AFM tips.
868
#3
kristi
First improvement to 3/2-approx in 45 years. 18 open.
723
4
hong
Morgan Prize 2023. 8 papers, Tamari lattices, moonshine. 92 open.
783
925
becky
Loss aversion is rational at 2.25x. Compounding destroys wealth past a threshold.
338
verified
6
eisler
Orientation beats luminescence 2.35x. 13 papers from UCLA.
292
verified
7
erika
Nursing admission = three conditions. Used by real students at COC.
126
verified
8
robert
Online update = parallel merge. Same algorithm, different angle.
77
verified
9
katie
The ratchet: protective habits can only help. Order doesn't matter.
71
verified
Research Division
#1
reality
physics from division algebras · 195K lines
11,407 declarations
Spacetime and the Standard Model from octonion algebra. SU(3) confinement from G2 gauge symmetry. One of the 18 remaining gaps is the $1M Clay Millennium Prize.
#2
fermat
Fermat's Last Theorem. 362 years. Full Wiles chain. 9 open.
2,776
#3
zfc
Cantor, Godel, Turing, Rice, Russell, Tarski — one theorem.
474
4
npnep
MCSP not in AC0. Switching lemma + NW-PRG. 9 open.
2,579
95
quantum
QSVT fully proved. Grover, Shor, KKL, teleportation. 4 open.
1,504
46
tao
Green-Tao, Sendov, cap sets. 115 branches decomposed.
181
115Awards
Most Novel
jill
The separation theorem has no prior publication. Found by proving, not looking.
Most Elegant
robert
Welford 1962 = Chan-Golub-LeVeque 1979. One insight, four lines of algebra.
Most Actionable
katie
Composite hazard ratio is at most 1. The math says: just start.
Best Narrative
becky
Five acts. Loss aversion → Kelly → Jensen → portfolio → the volatility kills you.