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.
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.
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.
You can just use another implementation nowadays.
(We don't know because we can't run AlphaGo to compare them).
In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs using Lean.
What is a nlinarith?
Docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib...
has the example:
0 ≤ x^2 if x : ℝ