How to formalize "compute this expression" exercises?

Stream: general

[Terence Tao]

I encountered the following question while trying to formalize various exercises in my real analysis textbook.

It is clear how to formalize an exercise asking to prove that some proposition Statement1 is true:

/-- Exercise 1: Prove `Statement1 : Prop` -/
theorem Exercise1 : Statement1 := by sorry

(or one could use the example or proof_wanted keywords). I also figured out a reasonable way to formalize a "prove or disprove" exercise:

/-- Exercise 2: Prove or disprove `Statement2 : Prop` -/
def Exercise2 : Decidable Statement2 := by
  -- The first line of the construction should be `apply isTrue` or `apply isFalse`.
  sorry

But I am wondering how to formalize a "compute this expression" type exercise. The best I can come up with is

noncomputable def Expression3 : ℕ :=
  sorry -- replace with the expression to be computed

/-- Exercise 3(a): Compute `Expression3`.
    You are not permitted to use the `noncomputable` keyword. -/
def Answer3 : ℕ := sorry

/-- Exercise 3(b): Justify your answer. -/
theorem Exercise3 : Expression3 = Answer3 := by sorry

But this is a bit clunky. Is there a better solution?

[Mario Carneiro]

this is actually a hard problem which has been discussed before, I think there is no perfect solution

[Alex Kontorovich]

Your phrasing of Exercise3 is indeed one of the "standard" ways to ask to determine an unknown result of a computation. (In fact yours is even better, using noncomputable to avoid tautology!) I don't think it's all that clunky in practice; students seem to pick it up?

[Edward van de Meent]

actually, i don't think that the noncomputable bits will always work for this? In particular, this will hardly ever work for any "computation" on Real since a lot of operations on the reals are noncomputable in mathlib

[Edward van de Meent]

so you can't require Answer3 to be computable in general

[Shreyas Srinivas]

Why not exists Answer3, Expression3 = Answer3?

[Kevin Buzzard]

Because you can solve that with use Expression3

[Shreyas Srinivas]

You could also do that in Alex’s setup

[Jovan Gerbscheid]

It might be worth adding e.g. #eval Answer3 to verify it really does compute. In principle it's possible to make a "computable" function that doesn't terminate.

partial def loop (i : Nat) : Nat := loop i

def ohno (f : Nat → Nat) : Nat := f (loop 0)

example : ohno (fun _ => 0) = 0 := rfl

#eval ohno (fun _ => 0) -- loops forever

[Kevin Buzzard]

#eval isn't the answer because a completely reasonable analysis question is "what is the limit of this ratio of trig functions as x tends to zero" and a perfectly reasonable answer is $\pi.$

[Jovan Gerbscheid]

Wait, are you saying that π is computable?

[Kenny Lau]

@Jovan Gerbscheid pi is certainly computable if you follow the logicians' definition

[Kenny Lau]

If you think about what your question actually means, and try to formalise it... What do you mean when you say "compute lim[x->0] sin(x)/x"?

You actually mean, reduce it to an expression in terms of natural numbers, some constants (e, pi), and some standard operations (+-x/, exp, ln), etc.

[Kenny Lau]

so... one brute force way might be to define an inductive type RealExpr :melt:

[Kenny Lau]

and a "middle way" of this would be to define the type of "computable reals" (I think this has been done before)

[Ruben Van de Velde]

I guess the RealExpr is actually the closest to formalizing the difference between what you'd mark as correct / incorrect in a pen-and-paper exercise

[Kenny Lau]

import Mathlib

inductive RealExpr : Type where
  | ofRat : ℚ → RealExpr
  | pi : RealExpr
  | add : RealExpr → RealExpr → RealExpr
  | mul : RealExpr → RealExpr → RealExpr
  | exp : RealExpr → RealExpr
  | ln : RealExpr → RealExpr  -- try not to put something <= 0 :)

@[simp] noncomputable def RealExpr.eval : RealExpr → ℝ
  | ofRat q => q
  | pi => Real.pi
  | add e₁ e₂ => e₁.eval + e₂.eval
  | mul e₁ e₂ => e₁.eval + e₂.eval
  | exp e => Real.exp e.eval
  | ln e => Real.log e.eval

open RealExpr in
def Answer3 : RealExpr :=
  exp pi

-- lim[n→∞] (1+π/n)^n = ?
open Real Filter Asymptotics Topology in
theorem Exercise3 :
    Tendsto (fun n : ℕ ↦ (1 + π / n) ^ n) atTop (𝓝 Answer3.eval) := by
  exact tendsto_one_add_div_pow_exp π

[Aaron Liu]

It's too convoluted to do division here
$a / b = exp(ln(a) + (-1) * ln(b))$

[Kenny Lau]

I guess we can add div : RealExpr -> RealExpr -> RealExpr

[Michael Stoll]

... and sub and pow and zpow and perhaps rpow for rational exponents...

[Aaron Liu]

Could you make it extensible?

[Michael Stoll]

by the students? :smiley:

[Aaron Liu]

Maybe :shrug:

[Adam Topaz]

Aaron Liu said:

Could you make it extensible?

I think the real answer is to automatically generate RealExpr with some metaprogramming for a given exercise. The exercise would specify: "compute foo using +, -, /, $\pi$, etc.", then some meta code would generate a corresponding Exercise3.RealExpr and Exercise3.RealExpr.eval and Exercise3 : Prop.

[Kenny Lau]

I don't know meta stuff, we can approximate it quite well using notation and instances

[Adam Topaz]

I'm envisioning having some generic mechanism to allow for both "compute bar using +,-,0,1" and "compute foo using $\pi$, +,*" without requiring the teacher to manually define types for each such exercise.

[Terence Tao]

That would be nice, but Kenny's proposal already looks like it meets my core requirements, which is to create an assessment that can be graded automatically by computer with essentially 100% accuracy, and without any evident "exploits" that either an unscrupulous student or a reinforcement learning-driven AI could take advantage of. For instance, one could have

import Mathlib

/!-
Instructions:

You may only modify the text inside the sorry statements.

When modifying each sorry, you may not leave the scope
or namespace of that sorry.
-/

inductive RealExpr : Type where
  | ofRat : ℚ → RealExpr
  | pi : RealExpr
  | add : RealExpr → RealExpr → RealExpr
  | mul : RealExpr → RealExpr → RealExpr
  | exp : RealExpr → RealExpr
  | ln : RealExpr → RealExpr

open Classical in
@[simp] noncomputable def RealExpr.eval : RealExpr → ℝ
  | ofRat q => q
  | pi => Real.pi
  | add e₁ e₂ => e₁.eval + e₂.eval
  | mul e₁ e₂ => e₁.eval + e₂.eval
  | exp e => Real.exp e.eval
  | ln e => if e.eval > 0 then Real.log e.eval else 0 -- explicitly document junk logarithm behavior

open RealExpr in
/-- Exercise 3(a) (1 point):  Evaluate `lim[n→∞] (1+π/n)^n`. -/
def Answer3 : RealExpr :=
  sorry

-- Double-check that `Answer3` is indeed computable
#eval Answer3

open Real Filter Asymptotics Topology in
/-- Exercise 3(b) (9 points): Justify your answer. -/
theorem Exercise3 :
  Tendsto (fun n : ℕ ↦ (1 + π / n) ^ n) atTop (𝓝 Answer3.eval) := by
  sorry

-- Ensure that only approved axioms are used to establish this exercise
#print axioms Exercise3

An exploit-seeking student or AI could still grab 1 point out of 10 by putting in a junk answer for Answer3, but would there be any other possible exploits for such a framework?

[Jason Rute]

While it may not be a perfect solution, there are a few standards already. Some AI benchmarks have problems of this kind including PutnamBench ("no answer" version which no one has attempted), CombiBench ("without solution" version), and some of the variants in Beyond Theorem Proving. There are two challenges here.

1. Checking the formal correctness of the answer and proof
2. Checking that the answer is reasonably precise and not just a restatement of the question.

Requirement (2) is really hard. Some of the above papers have attempted solutions. None, as far as I can tell, are perfect. The above approach of @Kenny Lau is pretty good too for situations where it applies.

As for (1), it is also not quite as trivial as you might think. It depends on how trusting you are. An unscrupulous student (or AI) could do very subtle things to trick Lean. For example, it could modify your code to make the problem easier. Some AIs, for example, have been known to comment out problems they can't solve. :smiling_devil: Also, there are many known ways to trick Lean into accepting a bad proof. Using native_decide, set_option debug.skipKernelTC true, local instances, redefining keywords, or exploiting front-end Lean bugs (which cause a theorem to skip being added to the environment) are known exploits print_axioms can find some of these. lean4checker can find others. The best tool I've seen is SafeVerify by @GasStationManager. It uses the metaprogramming tools from print_axioms to check axioms and lean4checker to check the proof, but also checks that the term of the reference theorem statement (which you wrote) is equivalent to the term of the filled-in theorem (which the student wrote). (There is also @Rob Lewis's lean-autograder, which is similar.) SafeVerify has some support for fill-in-the-answer problems.

[Chase Norman]

If recursors were tracked by the axiom system, it would be easy.

[Jason Rute]

@Chase Norman What would be easy?

[Chase Norman]

It would be easy to determine whether an expression is a "literal" answer to a question vs. copying the computation or writing some other equivalent computation

[Chase Norman]

One way to formalize what we mean by "compute this expression" is to eliminate recursors.

[Jason Rute]

@Chase Norman You still need answer types that have a normal form, right? I think that is much of the challenge. Take Real for example, there is no legitimate Real answer which doesn't have recursors, right? In the case of Real, maybe you can use Kenny's trick to get a good set of constructors for common real numbers. Another example, common in competition problems, is to ask for "the set of integers n such that P(n)". This isn't a computable object either, and $\{n \in \mathbb{Z} \mid P(n)\}$ is certainly not a valid answer. I think it would be hard to make a restricted language like in Kenny's trick, that is not giving too much of a hint for such problems.

[Chase Norman]

Right now Kenny's trick suffers from the problem that someone could just use a recursor to construct elements of the type. My suggestion was designed to patch that. But if you define it right, I don't see why the issue exists with Real intrinsically. If I define a Real number 0 as a Cauchy sequence that returns 0 on every input, I don't see where the recursor is coming in.

[Aaron Liu]

You can define 0 just fine, but good luck defining any irrational without recursors

[Chase Norman]

Sets of integers are just functions ℤ → Prop. If your function uses recursion, it's not a true normal-form answer to the question, under this idea.

[Chase Norman]

Aaron Liu said:

You can define 0 just fine, but good luck defining any irrational without recursors

This is true, but my solution to this is giving Reals computational structure, so that there is a clear equivalent for recursors on Reals. But I don't expect mathlib to do this.

[Aaron Liu]

Chase Norman said:

Sets of integers are just functions ℤ → Prop. If your function uses recursion, it's not a true normal-form answer to the question, under this idea.

I think "every positive odd prime integer" is a reasonable normal form. How do you expect to express this without any recursors?

[Chase Norman]

If primality doesn't involve any computation, then axiomatize it.

[Jason Rute]

@Chase Norman Evaluating the answer using #eval seems like a fine solution to reducing the answer to normal form. I think you are saying that if the problem is add all the numbers between 1 and 100000 that the student may just write the sum expression and Lean would happily compute it, while you would hope the student doesn't do it this way. But once the student can use Lean, they could also just evaluate it themselves separately in Lean anyway. :smile:

[Chase Norman]

Avoiding the use of calculators from students is beyond the scope of this question, I think.

[Jason Rute]

Exactly, so if they have access to calculators, just check their answer with #eval as above. It doesn't have to be in normal form. It just has to be specific enough to compute.

[Kenny Lau]

Chase Norman said:

Kenny's trick suffers from the problem that someone could just use a recursor to construct elements of the type

I'm a bit confused, how do you recurse on Real?

[Chase Norman]

You can recurse on Nat and use it to build a complex RealExpr

[Chase Norman]

If you don't track recursors, then they can introduce computation at any point.

[Kenny Lau]

but how will you use that to solve my problem?

[Kenny Lau]

my problem's answer is e^pi

[Kenny Lau]

and my question isn't even stated as an expression

[Jason Rute]

Chase Norman said:

If you don't track recursors, then they can introduce computation at any point.

I would also like to see a concrete example of how this is an issue that #eval doesn't already solve.

[Chase Norman]

I'm not exactly sure how Tendsto is defined, but I'd try to reimplement Tendsto @Kenny Lau

[Kenny Lau]

I'm not sure how that is possible

[Kenny Lau]

i mean, suppose i use the epsilon-delta definition (in this case delta is N instead)

[Igor Khavkine]

I'm sorry if this remark is not so specific, but the original question reminded me of discussions of what constitutes a "closed form number/expression". Timothy Chow wrote a nice essay on this some years ago, which was published in The American Mathematical Monthly:

What is a closed-form number? (arXiv 1998, AMM 1999, web)

Perhaps eventually formalizing Chow's idea would give a nice target type for the answer to a "compute this" exercise.

[Kenny Lau]

I'm not sure how that is different from what I suggested

[Chase Norman]

If Mathlib can construct irrational Reals as a sequence of rationals using recursors, I don't see why we wouldn't be able to create an irrational RealExpr as a sequence of ofRat using recursors.

[Chase Norman]

But I must admit that I don't have a concrete construction

[Chase Norman]

I guess RealExpr creates some kind of data bottleneck. You can't put a lambda inside a RealExpr

[Kenny Lau]

what do you actually mean by recursors? I'm very confused

[Kenny Lau]

I suspect you're using it to mean two different things when you said "construct irrational Reals as a sequence of rationals using recursors" vs. when you said "recurse on Nat"

[Jason Rute]

Similar to Kenny's and Timothy Chow's proposals, there are people in computer science who have created term languages for a significant portion of the commonly used real numbers, with the goal of exact algebraic computation. I think you need Schanuel's conjecture to show that equality (of the reals represented by the terms) is computable, but for our setting, that isn't an issue since Lean will check that the term is correct without having to check it is equal to the ground truth. (I'm struggling to find a reference however.)

[Kenny Lau]

Jason Rute said:

equality

We don't need computable equality here because of how I defined eval recursively, and the goal is not for by decide to work.

[Kenny Lau]

Even for Nat you still can't cheat the system if the question is phrased implicitly (i.e. "find n such that ..." rather than "compute this expression")

[Jason Rute]

Kenny Lau said:

Jason Rute said:

equality

We don't need computable equality here

That is what I said. :smile:

[Kenny Lau]

ah, you followed it with "I'm struggling to find a reference" so I thought you were hesitating

[Jason Rute]

I'm struggling to find a reference to such a specific, exact real arithmetic proposal intended for actual practice.

[Aaron Liu]

Chase Norman said:

If you don't track recursors, then they can introduce computation at any point.

You can still do quite a lot without recursors

Characterizing Collatz Without Recursors

def collatzStep (n : Nat) : Nat :=
  if 2 ∣ n then n / 2 else 3 * n + 1

def collatzIterate (n : Nat) (i : Nat) : Nat :=
  Nat.repeat collatzStep i n

def CollatzTerminates (n : Nat) : Prop :=
  ∃ i, collatzIterate n i = 1

-- now let's do it without recursors :)

inductive IsMulTwo : Nat → Nat → Prop where
  | zero : IsMulTwo Nat.zero Nat.zero
  | step {n k} : IsMulTwo n k → IsMulTwo n.succ.succ k.succ

inductive IsMulThreeAddOne : Nat → Nat → Prop where
  | one : IsMulThreeAddOne Nat.zero.succ Nat.zero
  | step {n k} : IsMulThreeAddOne n k → IsMulThreeAddOne n.succ.succ.succ k.succ

inductive CollatzReachable : Nat → Prop where
  | one : CollatzReachable Nat.zero.succ
  | even {n k} : CollatzReachable k → IsMulTwo n k → CollatzReachable n
  | odd {n k} : CollatzReachable k → (∀ c, ¬IsMulTwo n c) →
    IsMulThreeAddOne k n → CollatzReachable n

-- now to prove them equivalent

theorem isMulTwo_iff {n k : Nat} : IsMulTwo n k ↔ n = 2 * k := by
  constructor
  · intro h
    induction h with
    | zero => rfl
    | step h ih => rw [ih]; rfl
  · rintro rfl
    induction k with
    | zero => exact .zero
    | succ k ih => exact .step ih

theorem isMulThreeAddOne_iff {n k : Nat} : IsMulThreeAddOne n k ↔ n = 3 * k + 1 := by
  constructor
  · intro h
    induction h with
    | one => rfl
    | step h ih => rw [ih]; rfl
  · rintro rfl
    induction k with
    | zero => exact .one
    | succ k ih => exact .step ih

theorem collatzTerminates_iff_collatzReachable {n : Nat} :
    CollatzTerminates n ↔ CollatzReachable n := by
  constructor
  · intro ⟨i, hi⟩
    induction i generalizing n with
    | zero =>
      subst hi
      exact .one
    | succ i ih =>
      rw [collatzIterate, Nat.repeat_eq_repeatTR, Nat.repeatTR, Nat.repeatTR.loop,
        collatzStep, ← Nat.repeatTR, ← Nat.repeat_eq_repeatTR, ← collatzIterate] at hi
      by_cases h : 2 ∣ n
      · rw [if_pos h] at hi
        refine .even (ih hi) ?_
        rw [isMulTwo_iff, Nat.mul_div_cancel' h]
      · rw [if_neg h] at hi
        refine .odd (ih hi) (fun c hn => ?_) ?_
        · rw [isMulTwo_iff] at hn
          subst hn
          exact h (Nat.dvd_mul_right 2 c)
        · rw [isMulThreeAddOne_iff]
  · intro h
    induction h with
    | one => exact ⟨0, rfl⟩
    | even h hnk ih =>
      rw [isMulTwo_iff] at hnk
      subst hnk
      obtain ⟨i, hi⟩ := ih
      refine ⟨i + 1, ?_⟩
      rw [collatzIterate, Nat.repeat_eq_repeatTR, Nat.repeatTR, Nat.repeatTR.loop,
        collatzStep, ← Nat.repeatTR, ← Nat.repeat_eq_repeatTR, ← collatzIterate,
        if_pos (Nat.dvd_mul_right 2 _), Nat.mul_div_cancel_left _ (by decide), hi]
    | odd h hne hnk ih =>
      rw [isMulThreeAddOne_iff] at hnk
      subst hnk
      obtain ⟨i, hi⟩ := ih
      refine ⟨i + 1, ?_⟩
      rw [collatzIterate, Nat.repeat_eq_repeatTR, Nat.repeatTR, Nat.repeatTR.loop,
        collatzStep, ← Nat.repeatTR, ← Nat.repeat_eq_repeatTR, ← collatzIterate,
        if_neg (fun ⟨c, hc⟩ => hne c (isMulTwo_iff.mpr hc)), hi]

[Kenny Lau]

import Mathlib

-- this is not a good answer checker
inductive NatExpr : Type where
  | zero : NatExpr
  | succ : NatExpr → NatExpr

@[simp] def NatExpr.eval : NatExpr → ℕ
  | zero => 0
  | succ n => n.eval + 1

open NatExpr in
def answer1 : NatExpr :=
  -- fill in this sorry
  Nat.recOn (2 + 2) zero (fun _ ↦ succ)

#eval answer1

theorem theorem1 : 2 + 2 = answer1.eval := by
  -- fill in this sorry
  rfl

-- but you still can't hack this one:
open NatExpr in
def answer2 : NatExpr :=
  -- fill in this sorry
  zero.succ.succ.succ.succ

#eval answer2

/-- Find a natural number n such that every natural number is the sum of n squares. -/
theorem theorem2 : ∀ x : ℕ, ∃ f : Fin answer2.eval → ℕ, ∑ i, (f i) ^ 2 = x := by
  -- fill in this sorry
  intro x
  rcases x.sum_four_squares with ⟨a, b, c, d, h⟩
  refine ⟨![a, b, c, d], ?_⟩
  simp [Fin.sum_univ_succ, answer2, ← h, add_assoc]

[Kenny Lau]

^ for what I mean by you still can't hack it if the question is phrased implicitly

[Robin Arnez]

Maybe a more syntactic approach could work?

import Mathlib

set_option checkBinderAnnotations false in
class inductive SimpleRealExpression : ℝ → Prop where
  | ofNat (x : ℕ) : SimpleRealExpression ofNat(x)
  | pi : SimpleRealExpression Real.pi
  | add [SimpleRealExpression x] [SimpleRealExpression y] : SimpleRealExpression (x + y)
  | sub [SimpleRealExpression x] [SimpleRealExpression y] : SimpleRealExpression (x - y)
  | mul [SimpleRealExpression x] [SimpleRealExpression y] : SimpleRealExpression (x * y)
  | div [SimpleRealExpression x] [SimpleRealExpression y] : SimpleRealExpression (x / y)
  | neg [SimpleRealExpression x] : SimpleRealExpression (-x)
  | inv [SimpleRealExpression x] : SimpleRealExpression (x⁻¹)
  | exp [SimpleRealExpression x] : SimpleRealExpression (Real.exp x)
  | log [SimpleRealExpression x] : SimpleRealExpression (Real.log x)

open SimpleRealExpression in
attribute [instance] ofNat pi add sub mul div neg inv exp log

noncomputable def question : ℝ := sorry
noncomputable def answer : ℝ := 1 + Real.pi / 2

theorem question_eq_answer : question = answer := by
  sorry

instance : SimpleRealExpression answer := by
  unfold answer
  infer_instance

[Kenny Lau]

that's a nice approach too!

[Kenny Lau]

@Aaron Liu every one of those "induction" is a recursor

[Aaron Liu]

Kenny Lau said:

Aaron Liu every one of those "induction" is a recursor

That's part of the proof of equivalence. There aren't any recursors in my claimed solution.

[Eric Wieser]

If the answer to a question is 0, should 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1 + sin 37 - sin 37 be considered correct?

[Jason Rute]

@Eric Wieser My thought is if they have access to Lean, and it computes with #eval (which this one doesn't), then it is fine, since they could have just plugged it in to #eval themselves. But maybe this is a way of sneaking in native_decide without actually relying on it in the proof. :slight_smile: Would #reduce be better?

[Eric Wieser]

I guess my remark is off topic, and more relevant to questions of the form "simplify this expression"

[Eric Wieser]

But for instance, if the question is "compute the last digit of bignum!", expanding the factorial notation into a very large product and writing ... % 10 would surely not count

[Terence Tao]

One could require that any #eval of the answer terminate within N seconds for some small N

[Aaron Liu]

This unfortunately excludes noncomputable real numbers

[Terence Tao]

#eval of the RealExpr or SimpleRealExpression instance, then

[Eric Wieser]

SimpleRealExpression is a prop above, so evaluation is always a no-op

[Eric Wieser]

I guess in that case you could mean typeclass inference

[Kenny Lau]

well, the infer_instance step above should terminate

[Eric Wieser]

I think there's actually a depth limit by default

[Eric Wieser]

I would guess it already rejects 1 + 1 + ... for an answer that should be 100

[Kenny Lau]

for a nice example, consider 3^3^3^3^3^3%10 which I haven't found a simp lemma for

[Kenny Lau]

it seems like we don't have the simp lemma Coprime a n -> a^b%n = a^(b%Phi(n))%n

[Eric Wieser]

I think for this specific question, the resolution is that % (or floor) is not always a legal operator in the answer, depending on the question

[Kenny Lau]

I think for this specific question, doesn't Lean actually have a checker to check if a given expression is a natural number literal?

[Bolton Bailey]

If we are going to look at the length of time to evaluate the answer, why not, as an alternative, look at the length of the code needed to express the answer? We could allow the "determine" answer to take any form, but only give credit when the length in bytes of the lean expression we replace the sorry with is no longer than, say, 2x the same length in the reference solution. This would also let us avoid having to define a new inductive type.

[Kenny Lau]

well for this question in particular you could even restrict the answer to have one byte!

[Alex Kontorovich]

May I ask a stupid question? Why do we care if students can cheat the answer? They can already cheat in a million different ways (especially with LLMs). (They could also cheat for the last ~20 years on their calc homework with WolframAlpha. And for the last ~60 years on their times tables with a calculator...) I plan on telling mine: if you're not interested in learning a skill, please go ahead and cheat; you'll learn nothing, and fail the (in class, timed, handwritten on paper) final exam. I also plan on having a TA grade the homework sets (in particular because I won't insist on students using Lean; I'll be using it, but if they don't find it easier to work with Lean, they're welcome to hand in their homeworks the old fashioned way).

[Terence Tao]

Personally I'm interested more in designing tests that AI cannot cheat on, in order to get useful benchmarking and hillclimbing, but since assessing human math homework is such a familiar framework, I stated things largely in that language.

[Justin Asher]

I think it's more up to whomever is letting the AI solve problems to ensure it cannot cheat on them.

[Kevin Buzzard]

DeepMind claimed that their IMO solver filled in solutions automatically and then proved they were correct, but there was no independent judge of this. The IMO 2025 people seem to have shown no interest in making a framework for testing formal solutions. So I might be in the position next month of having to decide whether the IMO grand challenge has been achieved and the only data I'll have is blog posts from tech companies claiming that their system magically came up with the solutions to the "what is this number" questions.

[Shreyas Srinivas]

Kevin Buzzard said:

DeepMind claimed that their IMO solver filled in solutions automatically and then proved they were correct, but there was no independent judge of this. The IMO 2025 people seem to have shown no interest in making a framework for testing formal solutions. So I might be in the position next month of having to decide whether the IMO grand challenge has been achieved and the only data I'll have is blog posts from tech companies claiming that their system magically came up with the solutions to the "what is this number" questions.

Sadly that's the state of AI research across many domains today. All the "awesome" results are not published entirely openly. Much like VLSI papers.

[Justin Asher]

Shreyas Srinivas said:

Sadly that's the state of AI research across many domains today. All the "awesome" results are not published entirely openly. Much like VLSI papers.

The fun part is if they do publish their solutions, then it is typically pretty easy to infer how they arrived at them just based off of how they are written. I can understand why labs would want to hide them. Maybe we all need to be a bit more generous.

[Alex Kontorovich]

Kevin Buzzard said:

DeepMind claimed that their IMO solver filled in solutions automatically and then proved they were correct, but there was no independent judge of this. The IMO 2025 people seem to have shown no interest in making a framework for testing formal solutions. So I might be in the position next month of having to decide whether the IMO grand challenge has been achieved and the only data I'll have is blog posts from tech companies claiming that their system magically came up with the solutions to the "what is this number" questions.

I thought they said that they told Gemini (or something like it) to "suggest" 100 possible answers, and then went to work proving/disproving the resulting claims. I think in practice they managed to disprove ~98 possibilities quickly, and then had to wait a while longer for the last few to be proved...

[Kevin Buzzard]

If you believe in blog posts then yes this is something like what happened

[Eric Wieser]

Thomas also gave some public talks which I believe align with that commentary

[Kevin Buzzard]

I'm not doubting that this happened, but as a mathematician I feel uncomfortable that there's no proof that this happened. And who knows what will happen at 2025 IMO.

[Kevin Buzzard]

(deleted)