#Numina

Numina 做了个让人监督 AI 写 Lean 4 证明的工作台，还真拿它形式化了 Kakeya 猜想，开源版可以直接跑。