News for hackers. Stuff that matters.

A comment on AI solves IMO problems at silver medal level. Parent comment

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 ]