Gemini 3 pro performance on formal benchmarks

Stream: Machine Learning for Theorem Proving

[Ayush Agrawal]

Gemini 2.5 series were known to hallucinate alot on formal benchmarks. Do we know how Gemini 3 series perform on the same?

[Justin Asher]

I am super curious about this too, especially considering Google's emphasis on Lean programming through their various efforts, e.g., AlphaProof.

[Deleted User 968128]

https://epoch.ai/frontiermath
https://critpt.com/

Gemini 3 is significantly outperforming SOTA base models on advanced math and physics, however web and tool usage are compelling.

How Gemini 3 Pro Deep Think (a model which does a BFS using the base Pro model) will perform is what many are waiting to find out.

[Opt]

Tim Shephard said:

https://epoch.ai/frontiermath
https://critpt.com/

Gemini 3 is significantly outperforming SOTA base models on advanced math and physics, however web and tool usage are compelling.

How Gemini 3 Pro Deep Think (a model which does a BFS using the base Pro model) will perform is what many are waiting to find out.

I don't think we know what kind of search Deep Think does right? So we don't know if it's BFS or something else.

[Junyan Xu]

I find it interesting that Gemini 3 keeps hallucinating a certain McCoy's theorem saying that f.g. ideals in a commutative ring consisting of zerodivisors must be annihilated by some nonzero element, e.g. in this conversation and a previous one (which also shows a bug in extracting the final response from CoT).

[Deleted User 968128]

Opt said:

I don't think we know what kind of search Deep Think does right? So we don't know if it's BFS or something else.

Admittedly it is a bit of a simplification, but I'd argue it's definitely not DFS.

"Just as people tackle complex problems by taking the time to explore different angles, weigh potential solutions, and refine a final answer, Deep Think pushes the frontier of thinking capabilities by using parallel thinking techniques."
https://blog.google/products/gemini/gemini-2-5-deep-think/