4 ms·

> “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can und

> “The drive to mechanize proof and proof verification doesn’t strongly motivate most mathematicians as far as I can tell,” he [Michael Harris] said. “I can understand why computer scientists and logicians would be excited, but I think mathematicians are looking for something else.” I'm not a mathematician, but I have at times been able to consider myself a computer scientist. To me, the goal of "mechanizing" and formalizing mathematics seems instinctively recognizable as a worthwhile pursuit, for the same reason it's worth adding tests to an unwieldy legacy codebase: it makes it possible to refactor, to experiment and break things and see what happens. The more we formalize the most fundamental axioms and theorems of mathematics, the more confidently we can alter or remove them and see what happens to the rest of the system. Achieving "100% test coverage" and "instrumentation" of mathematics would allow us to analyze the system under stress. We could fuzz it. We could refactor it. We could even ask an AI to do that for us. As a relative layman, I'm often struck by how many mathematical theorems are dependent on the arbitrary paths we took to develop them. For the same reason, it's a common occurrence that one mathematician discovers an innovation in one branch of mathematics by simply borrowing a common technique from a distantly related branch. Those sorts of analogies and connections between ideas are difficult for humans to spot, and their discovery scales linearly with the number of mathematicians, who might prefer to spend their time discovering truly new ideas rather than repurposing those already existing ideas. But computers, on the other hand, are excellent at spotting these relationships, if given sufficiently formalized definitions of them. So that's why I'd be most excited about formalizing mathematics: how much low-hanging fruit is waiting to be discovered by computers that are just missing the right prompt?

giraj 3y ago
Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians. Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.
- TechBro8615 3y ago
  Well, as a computer scientist, I'd urge them to reconsider. :) My intuition is that, given a sufficiently formalized system, computers can help them achieve their goal of understanding and discovering more math, much more rapidly and with compounding effects. Although perhaps there is a risk that any mathematics the computer might "discover" would become increasingly incomprehensible to human mathematicians, in which case the discoveries wouldn't be worth much. I agree that humans are better at borrowing techniques between fields, but we can't do it quickly, and we can't systematically mine the entire "codebase" for these relationships (hence why "discoveries" in 2020 can combine ideas from 1990 and 2000). Besides, I suspect much of that gap between human and computer ability is due to a lack of a properly formalized representation of the ideas within each possibly related field. To use a programming term, it's a "code smell" if we haven't properly encoded the relationships between two fields. Sure, we can manually identify them, and then build on them once we do. But why did we need to bother in the first place? Wouldn't a formal system have made the relationships obvious, or at least more automatically discoverable? Large language models have also changed my view of what computers are capable of, and in that context I've been most impressed with their ability to analogize and explain relationships between seemingly arbitrary sets of ideas. It makes sense they'd be good at this, since the premise of training them is to construct a web of weights that's indecipherable to humans but fundamentally enabling to the language model. Stephen Wolfram has been writing about how language models seem to encode a certain "truth" which has always existed but which we've never recognized. This idea resonates with me and I expect models have a lot to teach us about our own consciousness and how we model the world. But on the other hand, if LLMs are so successful, by definition, at identifying relationships without being given formal representations of them, then why bother formalizing mathematics? After all, mathematics only exists because we can communicate its ideas by constructing the language of mathematics as a sort of amalgam of spoken language and abstractions we create within it. And while the exercise of formalizing the relationships between those abstractions might identify some imprecisions or mistaken assumptions in the existing hybrid of spoken language and formalized chunks of math, do we really need to bother? For an advanced LLM, shouldn't our existing definitions become naturally encoded into its weights during training, so that any emergent formalisms can be poked and prodded when we talk to it or ask it to reason about them? Or will it get stuck on the same imprecisions that we might identify when trying to manually formalize our existing systems of mathematics?
BSEdlMMldESB 3y ago
[flagged]
paulddraper 3y ago
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?
- giraj 3y ago
  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.
  - hgsgm 3y ago
    Most mathematicians don't care if proofs are correct, only that they look correct to other mathematicians.
    - giraj 3y ago
      That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.
- golol 3y ago
  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.

giraj 3y ago

Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math. The reasons you state for your interest in formalisation don't appeal to most mathematicians. Concerning analogies and borrowing techniques between fields, this is absolutely something humans are good at and which it is very hard for computers to do. Why do you think otherwise? To take a very simple example, most mathematical objects can be represented in different ways. A mathematician can fluently move between these representations, whereas computers cannot. This is a largely the obstacle for the adoption of proof assistants among mathematicians.

TechBro8615 3y ago
Well, as a computer scientist, I'd urge them to reconsider. :) My intuition is that, given a sufficiently formalized system, computers can help them achieve their goal of understanding and discovering more math, much more rapidly and with compounding effects. Although perhaps there is a risk that any mathematics the computer might "discover" would become increasingly incomprehensible to human mathematicians, in which case the discoveries wouldn't be worth much. I agree that humans are better at borrowing techniques between fields, but we can't do it quickly, and we can't systematically mine the entire "codebase" for these relationships (hence why "discoveries" in 2020 can combine ideas from 1990 and 2000). Besides, I suspect much of that gap between human and computer ability is due to a lack of a properly formalized representation of the ideas within each possibly related field. To use a programming term, it's a "code smell" if we haven't properly encoded the relationships between two fields. Sure, we can manually identify them, and then build on them once we do. But why did we need to bother in the first place? Wouldn't a formal system have made the relationships obvious, or at least more automatically discoverable? Large language models have also changed my view of what computers are capable of, and in that context I've been most impressed with their ability to analogize and explain relationships between seemingly arbitrary sets of ideas. It makes sense they'd be good at this, since the premise of training them is to construct a web of weights that's indecipherable to humans but fundamentally enabling to the language model. Stephen Wolfram has been writing about how language models seem to encode a certain "truth" which has always existed but which we've never recognized. This idea resonates with me and I expect models have a lot to teach us about our own consciousness and how we model the world. But on the other hand, if LLMs are so successful, by definition, at identifying relationships without being given formal representations of them, then why bother formalizing mathematics? After all, mathematics only exists because we can communicate its ideas by constructing the language of mathematics as a sort of amalgam of spoken language and abstractions we create within it. And while the exercise of formalizing the relationships between those abstractions might identify some imprecisions or mistaken assumptions in the existing hybrid of spoken language and formalized chunks of math, do we really need to bother? For an advanced LLM, shouldn't our existing definitions become naturally encoded into its weights during training, so that any emergent formalisms can be poked and prodded when we talk to it or ask it to reason about them? Or will it get stuck on the same imprecisions that we might identify when trying to manually formalize our existing systems of mathematics?

BSEdlMMldESB 3y ago

[flagged]

paulddraper 3y ago

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?

giraj 3y ago
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.
- hgsgm 3y ago
  Most mathematicians don't care if proofs are correct, only that they look correct to other mathematicians.
  - giraj 3y ago
    That is an extremely uncharitable take. I find that most mathematicians care deeply that their proofs are correct.
golol 3y ago
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.