Awe at ETH falling
Many are stunned that the Exponential Time Hypothesis, assumed in hundreds or thousands of papers, was disproved with a Lean-verified subexponential #SAT algorithm, and they debate what it means for P vs NP.
Verifiable domains favor AI
Commenters argue AI excels where cheap checks like Lean exist, while biology, chemistry and lab sciences remain bottlenecked by slow, expensive experiments.
Cynicism about PR and funding
Some see the collaborative framing and $5M fund as PR that bypasses peer review and pushes verification costs onto academics, while others credit OpenAI for improving on its last math release.