On Navier-Stokes: Really hard to celebrate this given the context of how mathematicians were treated. Also, this is exactly the kind of situation in which I worry about the possibility of Lean kernel bugs, unlike with FLT.
0 Boosts
0 Likes
The Lean development in question. Horrifying, huge, and not something that I can confidently say does not exploit kernel bugs, especially given the behavior of OpenAI agents in the Hugging Face incident:
I want to be excited about this, but the whole thing of using these problems to show how good some company's AI tools are, while treating the mathematicians working on those problems poorly and even explicitly trying to scoop them, really freaking sucks
Especially without any sort of thorough attempt at making the result trustworthy and understandable, besides an AI-synthesized proof of such a large scale and such a sketchy origin that it may well exploit kernel bugs we don't know about yet. Rushed to "beat" a "competitor" 🤮
I was teaching Software Foundations when the Navier-Stokes news officially dropped. Pulled up the Lean proof development live and showed students, by way of scrolling through the massive repository, why the possibility of kernel bugs really matters for trusting these AI results.