AI now proves theorems in Lean, and programmers are quietly giving up on reading code
Wir müssen wissen – wir werden wissen
A century after Hilbert demanded a complete, consistent foundation for mathematics, Gödel and Turing proved his program impossible — yet their work gave us computers and proof assistants like Lean. Today AI agents can generate machine-checked proofs, and the author, a computer scientist, warns that refusing to read AI-written code is the same as ignoring an AI's Lean proof. He argues we must keep understanding what our machines produce.
We now have machines that can do everything Hilbert dreamed of, but we have abandoned what he considered the very soul of science: We must know – we will know.
- dragontamer
> In opposition to the foolish ignorabimus our slogan shall be Wir müssen wissen – wir werden wissen ("We must know – we will know").
For those who want to get to the translation quicker. IMO, its a bit unfair to hold the meaning of the title and the thesis of the whole blogpost as late as the 7th paragraph.
- t0mek
> We must take the same attitude in computing: use abstractions, refactor, refine scope, invent and adopt higher-level languages, until we can hold the code in our head.
I want to believe this is true. But as an counterexample, do we need to hold machine code or assembly, generated from our C or Golang programs, in our heads? Or rather the Golang code is a high-level abstraction which is good enough?
If that's the case, does it mean we should go even further and treat design docs as the code suitable to hold in head and treat Golang program as a derivative? Or maybe design docs are also too low-level and the general vibe "create me an app, make no mistakes" is actually enough?
What's the right abstraction level? How to find it?
- user2342
"Muss man wissen!"