{c}
{title2=2024}

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
> AI achieves silver-medal standard solving <International Mathematical Olympiad> problems

Uses <autoformalization> down to <Lean>, and then <AlphaZero>. Cool.


AlphaProof

{c}
{tag=Neuro-symbolic AI}
{wiki}

https://harmonic.fun/

They seem to do <autoformalization>, <automated theorem proving> and <code generation>, and they use <Lean> a lot. Sounds fun.


harmonic.fun

"Autoformalization" refers to automatically converting a traditional human readable mathematical proof to a <formal proof>.

The topic received some attention with the <AI boom> and rise of <LLMs>:
* https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/autoformalization.3F.html


Ciro Santilli @cirosantilli 37

 Incoming links: Autoformalization