Any Gemini 3 experiences?

Stream: Machine Learning for Theorem Proving

[Geoffrey Irving]

One thing that occurs is that we’re now far enough into the existence of AlphaProof that Gemini may have intentionally oversampled Lean code to help the project, which might help with Cursor and similar, not just AlphaProof.

[Bas Spitters]

I'm wondering whether it is possible to make a model portable version of something like @Cameron Freer Lean Skills. The technology used exists in most modern models, but the models also tell me that it is non-trivial to port it from one model to another...
https://claudemarketplaces.com/plugins/cameronfreer-lean4-skills

[Matthew Ballard]

I would start by globally replacing Claude by Gemini in #Machine Learning for Theorem Proving > How have you guys found GPT 5? @ 💬

[Deleted User 968128]

Relevant to this thread as it details a mixture of Gemini 3 and GPT5: #Machine Learning for Theorem Proving > How have you guys found GPT 5? @ 💬

[Matthew Ballard]

One data point: it doesn’t generate a properly formatted unification hint.

[Eric Wieser]

I would guess that most members of this Zulip, myself included, cannot generate a correct unification hint

[Geoffrey Irving]

Indeed, what is a unification hint?

[Aaron Liu]

I've figured out what a unification hint is but not how they work or how to make one or when I should use them

[Geoffrey Irving]

I decided to Lean about them, so I asked Gemini 3. It gave me a reasonable explanation, and then the example code

-- 1. Define a simple structure (Magma)
structure Magma where
  carrier : Type
  mul : carrier → carrier → carrier

-- 2. Define a concrete instance for Nat
def NatMagma : Magma := {
  carrier := Nat
  mul := Nat.mul
}

-- 3. Define a notation or function that expects a Magma
-- This function takes a Magma `m` and two elements of its carrier
def genericMul {m : Magma} (x y : m.carrier) : m.carrier :=
  m.mul x y

-- 4. Try to use it with plain Nats
-- ERROR: Lean fails here.
-- It expects `genericMul` to determine `?m` from the arguments.
-- The arguments `3` and `4` are `Nat`.
-- Lean tries to solve: `m.carrier =?= Nat`
-- It cannot solve this "backward" (from projection to structure).
#check genericMul 3 4

-- Syntax: unif_hint (variables) where
--    Proposed_Solution
--    |- Problem_You_Are_Stuck_On

unif_hint (m : Magma) where
  m =?= NatMagma
  |- m.carrier =?= Nat

#check genericMul 3 4
-- Result: genericMul 3 4 : Nat
-- Lean successfully inferred that `m` must be `NatMagma`.

but the final check still doesn't work. I gave the error to Gemini, and it fixed it to

-- 2. This WORKS (Explicit annotation triggers the hint)
#check genericMul (3 : Nat) (4 : Nat)
-- Output: genericMul 3 4 : Nat

[Geoffrey Irving]

Certainly doesn't mean it can do unification hints in anger, but at least it knows more about them than I [did 10 minutes ago].

[Bas Spitters]

I believe this is the source of unification hints. https://link.springer.com/chapter/10.1007/978-3-642-03359-9_8
This let to the integration of ELPI logic programming language in Rocq, which can be used to implement canonical structures, type classes and coercions...