Comment by cyode

I saw the 1996 FLT documentary in high school calculus class. For me, it forever cemented that archetype of modern math researcher at the top of my mental “smart” totem pole.

It also convinced me I had no interest in that path. Setting aside the grinding work of producing a proof that can only be reached by existing years in the abstract and hyper niche isolation of the problem space (not to mention that you might never discover it or that it DNE), the anguish of the output being a paper or presentation or some other artifact of human symbology (_words_, really) that could at any moment be refuted by a single observation of a single mistake—-that sounded like hell to me.

An equivalent high schooler today probably sees things differently, in light of this news and the undeniable implications of LLMs on mathematics. Sturdy autoformalization tooling should with time completely dispel the aforementioned anguish, once our confidence in converting a human proof to Lean/etc. reaches that of a compiler translating Java application language to bytecode. Errata may always exist, but in practice these new methods will do wonders for rigor and peace of mind.

(I’m far less confident re novel discoveries. There’s too much chance of derivative findings based on something part of the training looking like genius but really just tiptoeing on the shoulders of humans, whereas autoformalization is absolutely convincing to me as transformative, particularly to check correctness of AI outputted proofs as mentioned in the post.)