3 ms·

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the

> This story really highlights, to me, the poor job which humans do of documenting modern mathematics. There appear to be so many things which are “known to the experts” but not correctly documented. The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. For me, this is just one of many reasons why humans might want to consider getting mathematics written down properly, i.e. in a formal system, where the chances of error are orders of magnitude smaller. However most mathematicians are not formalists, and for those people I need to justify my work in a different way. For those mathematicians, I argue that teaching machines our arguments is a crucial step towards getting machines to do it themselves. Until then, we seemed to be doomed to fix up human errors manually. It makes me think about how you get UI/UX/web designers who make (informal, imprecise) mockups and prototypes of their design ideas and interaction flows, they then hand these off to a developer to do the coding (formalise it, explain it precisely to the machine), and on the way the developer will inevitably find problems/holes in the designs (like an interaction scenario or code path not considered in the design, which could uncover a major design flaw), which the developer and/or the designer will have to patch somehow. As in, design and development are different roles and require different mindsets, and most designers have a very strong resistance against working and thinking like a developer.

coliveira 2y ago
> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.
- hansvm 2y ago
  TFA isn't about AI; it's about taking the same arguments mathematicians are already writing down semi-formally with a hand-wavy argument that it could be made completely formal, and instead/also writing them down formally. In cases where the Hilbert machine applies, the mathematician writing down the semi-formal argument already has to state the new axioms, justify them, and reason about how they apply, and the proposal would just take that "reason about how they apply" step and write it in a computer-verifiable way.
- ur-whale 2y ago
  > This was already tried, and failed (Hilbert) Who likely underestimated how hard it would be. And who didn't have a 2024 computer on hand.
  - jmpetroske 2y ago
    The reason Hilbert failed is because it’s mathematically impossible (Gödels incompleteness theorem).
    - ur-whale 2y ago
      > because it’s mathematically impossible I guess the Lean devs can all pack and go home then. Also: how could they possibly miss Gödel's theorem, how careless of them.
      - jmpetroske 2y ago
        Look, you’re taking my response out of context. I’m just stating that the reason Hilbert failed is not that he didn’t have a computer. Lean devs aren’t trying to do what Hilbert was.
- lambdaone 2y ago
  While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English. Nor is this in any way "a fundamental problem with using AI to do math".
  - tialaramex 2y ago
    The other end of the Church-Turing intuition is that if we couldn't possibly do it then the machines can't do it either. What they're doing is the same, it's not only not magically less powerful it's also not not magically more powerful. You seem to be imagining that Gödel is just a small problem you can carve off and ignore, but it applies for everything powerful enough to do arithmetic. Of course we can have the AI muddle along with intuition, but that's not actually an improvement, our mathematicians can already use intuition and they've got a lot more experience.
  - youoy 2y ago
    It's a fundamental problem with using AI to do "intuitive" math, but not a fundamental problem with AI to do formal math. As you have stared, a lot of mathematics can be formalized. For me the problem for AI with math is going to be the generative part. Validating a proof or trying to come up with a proof for a given statement may be within reach. Coming up with meaningful/interesting statements to proof is another completely different story.
  - lisper 2y ago
    There are two problems with this. First, writing something down in English is very different from formalizing it. Natural language interacts with human brains in all kinds of complicated ways that we do not fully understand, so just because we can make a compelling-sounding argument in English doesn't mean that argument doesn't have holes somewhere. Second, the incompleteness theorems apply only to given formal systems, not to formality in general. Given a system, you can produce a Godel sentence for that system. But any Godel sentence for a given system has a proof in some other more powerful system. This is trivially true because you can always add the Godel sentence for a system as an axiom. This is a very common misconception about math even among mathematicians. Math produces only conditional truths, not absolute ones. All formal reasoning has to start with a set of axioms and deduction rules. Some sets of axioms and rules turn out to be more useful and interesting than others, but none of them are True in a Platonic sense, not even the Peano axioms. Natural numbers just happen to be a good model of certain physical phenomena (and less-good models of other physical phenomena). Irrational numbers and complex numbers and quaternions etc. etc. turn out to be good models of other physical phenomena, and other mathematical constructs turn out not to be good models of anything physical but rather just exhibit interesting and useful behavior in their own right (elliptic curves come to mind). None of these things are True. At best they are Useful or Interesting. But all of it is formalizable.
- zozbot234 2y ago
  Hilbert's program assumed math to be completely decidable, i.e. that for every possible statement, a decision procedure could tell whether it was true or false. We know now that no such procedure can possibly exist. But merely writing down all known math in a formal system is completely doable. (Of course, formalization systems can be used to state any additional axioms that may be required of any given argument or development, so the original concerns about incompleteness are just not very relevant.)
- naasking 2y ago
  > So this points to a fundamental problem with using AI to do math. No it doesn't, AI like an LLM has no issues with stating two inconsistent propositions, just like humans, which is why both AI and humans can reason about all of mathematics, eg. Godel theorems is that a formal system cannot simultaneously be complete and consistent.

coliveira 2y ago

> consider getting mathematics written down properly, i.e. in a formal system This was already tried, and failed (Hilbert). In the aftermath of the failure we learned that mathematics cannot be completely formalized. So this points to a fundamental problem with using AI to do math.

hansvm 2y ago
TFA isn't about AI; it's about taking the same arguments mathematicians are already writing down semi-formally with a hand-wavy argument that it could be made completely formal, and instead/also writing them down formally. In cases where the Hilbert machine applies, the mathematician writing down the semi-formal argument already has to state the new axioms, justify them, and reason about how they apply, and the proposal would just take that "reason about how they apply" step and write it in a computer-verifiable way.
ur-whale 2y ago
> This was already tried, and failed (Hilbert) Who likely underestimated how hard it would be. And who didn't have a 2024 computer on hand.
- jmpetroske 2y ago
  The reason Hilbert failed is because it’s mathematically impossible (Gödels incompleteness theorem).
  - ur-whale 2y ago
    > because it’s mathematically impossible I guess the Lean devs can all pack and go home then. Also: how could they possibly miss Gödel's theorem, how careless of them.
    - jmpetroske 2y ago
      Look, you’re taking my response out of context. I’m just stating that the reason Hilbert failed is not that he didn’t have a computer. Lean devs aren’t trying to do what Hilbert was.
lambdaone 2y ago
While it's true that mathematics cannot ever be completely formalized, per Gödel's incompleteness theorems, a huge amount of it obviously can, as is demonstrated by the fact that we can write it down in a reasonably rigorous way in a combination of conventional mathematical notation and plain English. Nor is this in any way "a fundamental problem with using AI to do math".
- tialaramex 2y ago
  The other end of the Church-Turing intuition is that if we couldn't possibly do it then the machines can't do it either. What they're doing is the same, it's not only not magically less powerful it's also not not magically more powerful. You seem to be imagining that Gödel is just a small problem you can carve off and ignore, but it applies for everything powerful enough to do arithmetic. Of course we can have the AI muddle along with intuition, but that's not actually an improvement, our mathematicians can already use intuition and they've got a lot more experience.
- youoy 2y ago
  It's a fundamental problem with using AI to do "intuitive" math, but not a fundamental problem with AI to do formal math. As you have stared, a lot of mathematics can be formalized. For me the problem for AI with math is going to be the generative part. Validating a proof or trying to come up with a proof for a given statement may be within reach. Coming up with meaningful/interesting statements to proof is another completely different story.
- lisper 2y ago
  There are two problems with this. First, writing something down in English is very different from formalizing it. Natural language interacts with human brains in all kinds of complicated ways that we do not fully understand, so just because we can make a compelling-sounding argument in English doesn't mean that argument doesn't have holes somewhere. Second, the incompleteness theorems apply only to given formal systems, not to formality in general. Given a system, you can produce a Godel sentence for that system. But any Godel sentence for a given system has a proof in some other more powerful system. This is trivially true because you can always add the Godel sentence for a system as an axiom. This is a very common misconception about math even among mathematicians. Math produces only conditional truths, not absolute ones. All formal reasoning has to start with a set of axioms and deduction rules. Some sets of axioms and rules turn out to be more useful and interesting than others, but none of them are True in a Platonic sense, not even the Peano axioms. Natural numbers just happen to be a good model of certain physical phenomena (and less-good models of other physical phenomena). Irrational numbers and complex numbers and quaternions etc. etc. turn out to be good models of other physical phenomena, and other mathematical constructs turn out not to be good models of anything physical but rather just exhibit interesting and useful behavior in their own right (elliptic curves come to mind). None of these things are True. At best they are Useful or Interesting. But all of it is formalizable.
zozbot234 2y ago
Hilbert's program assumed math to be completely decidable, i.e. that for every possible statement, a decision procedure could tell whether it was true or false. We know now that no such procedure can possibly exist. But merely writing down all known math in a formal system is completely doable. (Of course, formalization systems can be used to state any additional axioms that may be required of any given argument or development, so the original concerns about incompleteness are just not very relevant.)
naasking 2y ago
> So this points to a fundamental problem with using AI to do math. No it doesn't, AI like an LLM has no issues with stating two inconsistent propositions, just like humans, which is why both AI and humans can reason about all of mathematics, eg. Godel theorems is that a formal system cannot simultaneously be complete and consistent.