AI solves IMO problems at silver medal level

Re:AI solves IMO problems at silver medal level by Ericson2314 on Thursday July 25, 2024 @12:02PM (#41070218)

The lede is a bit buried: they're using Lean!

This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general.

Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Smaug123 on Thursday July 25, 2024 @12:06PM (#41070274)

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`.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Ericson2314 on Thursday July 25, 2024 @12:58PM (#41070851)

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

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by ComplexSystems on Thursday July 25, 2024 @05:38PM (#41073668)

This is the greatest idea ever. Why doesn't this exist?

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by panagathon on Thursday July 25, 2024 @06:11PM (#41073919)

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.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by sebzim4500 on Thursday July 25, 2024 @07:28PM (#41074526)

If the tools are the same as the ones AlphaProof gets (i.e. a lean compiler) then no one would use them.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Ericson2314 on Friday July 26, 2024 @08:03PM (#41083446)

Well, hopefully that changes soon :)

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Davidzheng on Thursday July 25, 2024 @01:39PM (#41071271)

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

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by YeGoblynQueenne on Friday July 26, 2024 @06:54AM (#41077561)

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).

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by lucioperca on Friday July 26, 2024 @08:13AM (#41077948)

https://github.com/leela-zero/leela-zero

You can just use another implementation nowadays.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by YeGoblynQueenne on Friday July 26, 2024 @03:23PM (#41081463)

And how does Leela compare to AlphaGo?

(We don't know because we can't run AlphaGo to compare them).

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by wslh on Friday July 26, 2024 @09:13AM (#41078358)

> 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.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by xrisk on Thursday July 25, 2024 @01:44PM (#41071316)

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?

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by llwu on Thursday July 25, 2024 @02:07PM (#41071540)

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...

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by empath75 on Thursday July 25, 2024 @01:45PM (#41071326)

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.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by sebzim4500 on Thursday July 25, 2024 @03:33PM (#41072472)

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

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by gowld on Friday July 26, 2024 @05:59PM (#41082689)

That's not necessarily an edge. 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.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Ericson2314 on Thursday July 25, 2024 @12:05PM (#41070255)

They're def gonna go after the Riemann hypothesis with this, hehe.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by nwoli on Thursday July 25, 2024 @12:18PM (#41070430)

Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Smaug123 on Thursday July 25, 2024 @12:22PM (#41070461)

I think you might be thinking of the recent project to start Fermat's Last Theorem? The Riemann hypothesis has been easy to state (given what's in Mathlib) for years.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by Davidzheng on Thursday July 25, 2024 @01:39PM (#41071276)

Yeah lol i don't think either is hard to formalize in lean

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by raincole on Thursday July 25, 2024 @04:03PM (#41072764)

They're not just formalizing Fermant's Last Theorem's statement itself. They're formalizing the proof.

[ Parent | on HN ]

Re:AI solves IMO problems at silver medal level by queuebert on Thursday July 25, 2024 @03:04PM (#41072191)

That's amazing. I was just about to comment that hooking this up to Lean [1] would be killer. This must be the way forward for higher math, as proofs are getting so complicated that almost no one understands all pieces of major proofs.

1. https://lean-lang.org/

[ Parent | on HN ]