Similar to OpenAI’s neural theorem prover and Google’s Minerva, Meta AI unveiled with HTPS (HyperTree Proof Search) a model that was able to solve several International Math Olympiad (IMO) problems. Meta made their model available through the Lean Visual Studio Code (VSCode) plugin, that allows everyone to evaluate it within the Lean theorem prover assistant.