4 ms·

And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be construc

And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.

Ericson2314 2y ago
Hehe, well, we'll need to have a tool-assited international math Olympiad then.
- ComplexSystems 2y ago
  This is the greatest idea ever. Why doesn't this exist?
  - panagathon 2y ago
    This does sound like a lot of fun. Since this AI only reaches silver level, presumably such a contest could be quite competitive, with it not yet being clear cut whether a human or a tool-assisted human would come out on top, for any particular problem.
- sebzim4500 2y ago
  If the tools are the same as the ones AlphaProof gets (i.e. a lean compiler) then no one would use them.
  - Ericson2314 2y ago
    Well, hopefully that changes soon :)
Davidzheng 2y ago
Good. I want my AI to use all the advantages it has to reinvent the landscape of mathematics
- YeGoblynQueenne 2y ago
  Sure but note that's not "your AI". It's a closed-source, proprietary system by DeepMind who typically publish a result to reap the hype and then bury the system forever (see AlphaGo).
  - lucioperca 2y ago
    https://github.com/leela-zero/leela-zero https://github.com/leela-zero/leela-zero You can just use another implementation nowadays.
    - YeGoblynQueenne 2y ago
      And how does Leela compare to AlphaGo? (We don't know because we can't run AlphaGo to compare them).
- wslh 2y ago
  > I want my AI to use all the advantages it has to reinvent the landscape of mathematics The interesting thing about math, or science, and art in general, comparing it to games like chess or go is that science gives you the freedom to continue to excel as a human while in games we have lost the game and/or the league. Science and art are infinite and no AI can produce infinity.
xrisk 2y ago
Can you give some context on how using Lean benefits? In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs using Lean. What is a nlinarith?
- llwu 2y ago
  nlinarith is a proof automation that attempts to finish a proof using the simplex method to find a linear combination of hypotheses and things that have already been proven, as well as some quadratic terms of them. Docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Linarith/Frontend.html#tacticNlinarith!_ https://leanprover-community.github.io/mathlib4_docs/Mathlib...
empath75 2y ago
Don't think of lean as a tool that the ai is using (ie, cheating), think of lean plus AlphaProof as a single system. There's no reason to draw artificial boundaries around where the AI is and where the tools that the AI is using are. Lean itself is a traditional symbolic artificial intelligence system. People want always knock generative AIs for not being able to reason, and we've had automated systems that reason perfectly well for decades, but for some reason that doesn't count as AI to people.
sebzim4500 2y ago
The uses of `nlinarith` are very straight forward manipulations of inequalities, they would be one or two steps for a human too.
gowld 2y ago
That's not necessarily an edge. https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_C/tactics/nlinarith.html https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-math... has the example: 0 ≤ x^2 if x : ℝ which humans simply use without proof. The IMO doesn't challenge participants to prove everything, only the main ideas.

Ericson2314 2y ago

Hehe, well, we'll need to have a tool-assited international math Olympiad then.

ComplexSystems 2y ago
This is the greatest idea ever. Why doesn't this exist?
- panagathon 2y ago
  This does sound like a lot of fun. Since this AI only reaches silver level, presumably such a contest could be quite competitive, with it not yet being clear cut whether a human or a tool-assisted human would come out on top, for any particular problem.
sebzim4500 2y ago
If the tools are the same as the ones AlphaProof gets (i.e. a lean compiler) then no one would use them.
- Ericson2314 2y ago
  Well, hopefully that changes soon :)

Davidzheng 2y ago

Good. I want my AI to use all the advantages it has to reinvent the landscape of mathematics

YeGoblynQueenne 2y ago
Sure but note that's not "your AI". It's a closed-source, proprietary system by DeepMind who typically publish a result to reap the hype and then bury the system forever (see AlphaGo).
- lucioperca 2y ago
  https://github.com/leela-zero/leela-zero https://github.com/leela-zero/leela-zero You can just use another implementation nowadays.
  - YeGoblynQueenne 2y ago
    And how does Leela compare to AlphaGo? (We don't know because we can't run AlphaGo to compare them).
wslh 2y ago
> I want my AI to use all the advantages it has to reinvent the landscape of mathematics The interesting thing about math, or science, and art in general, comparing it to games like chess or go is that science gives you the freedom to continue to excel as a human while in games we have lost the game and/or the league. Science and art are infinite and no AI can produce infinity.

xrisk 2y ago

Can you give some context on how using Lean benefits? In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs using Lean. What is a nlinarith?

llwu 2y ago
nlinarith is a proof automation that attempts to finish a proof using the simplex method to find a linear combination of hypotheses and things that have already been proven, as well as some quadratic terms of them. Docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Linarith/Frontend.html#tacticNlinarith!_ https://leanprover-community.github.io/mathlib4_docs/Mathlib...

empath75 2y ago

Don't think of lean as a tool that the ai is using (ie, cheating), think of lean plus AlphaProof as a single system. There's no reason to draw artificial boundaries around where the AI is and where the tools that the AI is using are. Lean itself is a traditional symbolic artificial intelligence system. People want always knock generative AIs for not being able to reason, and we've had automated systems that reason perfectly well for decades, but for some reason that doesn't count as AI to people.

sebzim4500 2y ago

The uses of `nlinarith` are very straight forward manipulations of inequalities, they would be one or two steps for a human too.

gowld 2y ago

That's not necessarily an edge. https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_C/tactics/nlinarith.html https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-math... has the example: 0 ≤ x^2 if x : ℝ which humans simply use without proof. The IMO doesn't challenge participants to prove everything, only the main ideas.