The maths goes over my head, but this paragraph was very interesting:<p>> Tao then kicked off an effort to formalize the proof in Lean, a programming language that helps mathematicians verify theorems. In just a few weeks, that effort succeeded. Early Tuesday morning of December 5, Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step. This is the highest-profile use of such verification tools since 2021, and marks an inflection point in the ways mathematicians write proofs in terms a computer can understand. If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, said Gowers.
Yesterday I was wondering if it's possible to have an AI that can "recreate" the mathematics as we know it, and even go further and explore unexplored paths.<p>Though prduced by a video explaining how AI helped to find optimization in the computation of matrix multiplication.
You always hear "the map is not the territory". Which is to say, names are applied, models are asserted and all our fine ideas about the world are our own contrivance, not the world's.<p>But how close could we get?
10 years ago a crack professor unit was defunded by an academic tribunal for misconduct they didn't commit. These men promptly escaped from a maximum teaching schedule to the research underground. Today, still wanted by the activist community, they survive as proovers of fortune. If you have a problem that no one else can solve, and if you can find them, maybe you can hire The A-Team.