Hacker News Reader

Comment by paulddraper | Hacker News Reader

The questionable assumption is that mechanized proofs are useful in the first place.

Computer programs are useful. Bigly. So we develop infrastructure around them.

Are mechanized proofs useful? Are they intelligible? Do they grant insight? Do they work better?

Mechanized proofs ensure the correctness of the results they prove. That's useful. Indeed, the point of the article was that Voevodsky sought out proof assistants in order to ensure his math was correct.

As for your other questions: No, formal proofs are not intelligible to the average mathematician. They do not on their own grant insights, but the process of formalising a proof does often yield insights. (I speak from experience.) Not sure what you mean by "better"; they certainly don't replace ("informal") mathematical proofs.

Most mathematicians don't care if proofs are correct, only that they look correct to other mathematicians.

That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.

The formalized proofs are useful because they allow you to formalize more difficult proofs. That's circular but let me explain. Formalizing all of mathematics in a formal, computer verifiable language is theoretically easy. The problem is that you don't want it to take forever to write down a proof because you have to go axiom by axiom. This is a problem of abstraction. Just like we need programming languages which have powerful, high level methods of abstraction, like functions, we need a formal language for mathematics that makes it easy to formalize proofs. You don't want to work with the axioms all the time, but instead use your oreviously proven results. When you have a good setup like this, writing down a proof formally should only take O(n) time, meaning it only takes up to some constant longer than writing down the informal proof. The goal right now is to get this constant down so it becomes appealing for the average mathematician to formalize their proof, without needing deep knowledge of type theory. This is happening right now with the Mathlib of Lean, a database of already formalized theory.

So where does this lead? As you build a large database of formalized mathematics you get some snowball effects. We can train language models just like on code to assist us. Formalizing natural language mathematics should merely be a process of translation, if set up correctly, not somwthing computationally advanced. Copilot for formal maths will being the constant lower. As correctness of formal proofs can be automatically checked, at some point you can let the system attempt formalizing Pdf documents by itself. This yields you a larger database, more traininf data etc. In 20 years I hope that we have a database of most.mathematics formalized in Lean, and language models that can translate between natural language math and Lean quite fluently. As any formal language of mathematics is also a programming language, we van start doing some very serious program correctness validation. You will not just run your Euler iteration until it has sufficiently small error, but you will instead run it up to your PROVEN desired error. Because we did all the work of formalizing mathematics, this will not be much harder than just writing the program normally. Mathematicians can also now work with these systems and thereby work quicker, saving time on reviews. Computer verified proofs will.not be unreadable, the database will be open source and constantly refactored and kept clean. Etc. Etc.

I think you believe all this, but it just doesn't pass the smell test.

Are computer programs written this way?

No. (Or not yet.)

Well my whole point is that you have to build up a large codebase of formalized mathematics first, and you have to do it in an elegant way so it is easy to work with. Then verified programs is something we can start to realistically consider. But of course we can't do that yet (except in certain situations with great effort). It's really very similar to building up a whole software architecture. 30 years ago we were at machine code, now we are at maybe C. We want to get to the Figma of formalized mathematics. It will take many years but I don't see and conceptual hurdle, especially given the power of LLMs now.

Reply on news.ycombinator.com