comparing formal proofs of aime_1984_p1

11 Aug, 2025

(I work at Anthropic, but far from any efforts related to math reasoning or formalization; opinions are my own)

This is an incredibly specific rabbit-hole I fell into in 2022 but never wrote up, which I was reminded of while thinking about LLMs' math abilities recently. I don't think it provides any direct signal about how good they are today, but there might be something to take away about how we frame the question.

In February 2022, Polu et al. trained a GPT-3–like model to solve some formal math problems. They commented that the model's proof for the problem aime_1984_p1 was "rather short" (p. 25) compared to a human formalization. The problem:

(AIME 1984 P1) Find the value of $a_{2} + a_{4} + a_{6} + a_{8} + \dots + a_{98}$ if $a_{1}, a_{2}, a_{3} \dots$ is an arithmetic progression with common difference 1, and $a_{1} + a_{2} + a_{3} + \dots + a_{98} = 137$ .

The formalized statement (which provides the answer and just asks to prove it) and the model's proof:

theorem aime_1984_p1
  (u : ℕ → ℚ)
  (h₀ : ∀ n, u (n + 1) = u n + 1)
  (h₁ : ∑ k in finset.range 98, u k.succ = 137) :
  ∑ k in finset.range 49, u (2 * k.succ) = 93 :=
begin
  revert_all,
  simp [finset.sum_range_succ],
  ring,
  simp [pow_succ, mul_comm, add_left_comm, add_assoc],
  simp [two_mul],
  rintro p,
  revert p,
  simp [add_comm],
  intros p hp,
  simp [hp], ring_nf,
  intros,
  nlinarith
end

For a human, the trick to solving this problem is noticing that the desired expression $S : = a_{2} + a_{4} + a_{6} + a_{8} + \dots + a_{98}$ is closely related to $S^{'} : = a_{1} + a_{3} + a_{5} + a_{7} + \dots + a_{97}$ .

Every term in $S$ is one after the corresponding term in $S^{'}$ , and therefore one more than it. Thus, $S = S^{'} + 49$ .
But also, $S$ and $S^{'}$ together cover every term in the known sum $a_{1} + a_{2} + a_{3} + a_{4} + \dots + a_{98}$ exactly once, so $S + S^{'} = 137$ .

Solving the two equations gives the answer. This approach roughly describes the linked human formalization as well.

Why is the machine's proof shorter? The formalization writes the problem condition as $\sum_{k = 0}^{97} a_{k + 1} = 137$ and the goal as $\sum_{k = 0}^{48} a_{2 (k + 1)}$ , and finset.sum_range_succ is roughly the following identity:

\sum_{k = 0}^{n + 1} f (k) = f (n + 1) + \sum_{k = 0}^{n} f (k) . (†)

The step simp [finset.sum_range_succ] repeatedly simplifies the problem by applying this identity. $97 = 96 + 1$ , so $\sum_{k = 0}^{97} a_{k + 1}$ gets simplified to $a_{98} + \sum_{k = 0}^{96} a_{k + 1}$ . But $96 = 95 + 1$ , so that gets simplified to $a_{98} + a_{97} + \sum_{k = 1}^{96} a_{k}$ . And so on. The same simplification applies repeatedly to the goal expression. So, this step expands both sums into explicitly written out lists of 98 and 49 terms, respectively.

The next important step is simp [hp], which here repeatedly simplifies the problem by applying the property that

a_{n + 1} = a_{n} + 1 . (‡)

So $a_{98}$ is simplified to $a_{97} + 1$ , which is simplified to $a_{96} + 2$ , which is simplified to $a_{95} + 3$ , and so on, until we get $a_{0} + 98$ .¹ This happens to every other term too. After all that simplification, the condition and goal are both just linear in $a_{0}$ , and the proof can be finished with standard Lean steps.

To summarize, I would describe the model's solution informally as:

By repeatedly applying $(†)$ and $(‡)$ a few hundred times each, we can simplify the given condition to $98 a_{0} + 4851 = 137$ and the expression we're computing to $49 a_{0} + 2450$ . Solving the equation for $a_{0}$ and plugging it into the expression gives the answer.

To be clear, a human could solve the problem in a superficially similar way by writing $\sum_{k = 0}^{97} a_{k + 1} = \sum_{k = 0}^{97} (a_{0} + k + 1) = 98 a_{0} + \sum_{k = 0}^{97} (k + 1),$ then evaluating $\sum_{k = 0}^{97} (k + 1)$ by recognizing that it's a triangular number, so it equals $\frac{98 \cdot 99}{2} = 4851$ . This is not what the proof does. Even though it has few steps, when those steps are executed during verification, each $a_{k + 1}$ is turned into $a_{0} + k + 1$ as a separate computation, and then the constants are added together one by one to produce 4851, just as with, say, the Python expression sum(i + 1 for i in range(97)).

Given this strategy, the model's proof is actually rather circuitous. A briefer formalization (that works in the same version of Lean):

theorem aime_1984_p1
  (u : ℕ → ℚ)
  (h₀ : ∀ n, u (n + 1) = u n + 1)
  (h₁ : ∑ k in finset.range 98, u k.succ = 137) :
  ∑ k in finset.range 49, u (2 * k.succ) = 93 :=
begin
  revert h₁,
  simp [finset.sum_range_succ, two_mul, h₀],
  intros,
  nlinarith
end

appendix: technical notes on reproduction

Lean 3 has been deprecated (in favor of Lean 4) for a year or two, so verifying these proofs today is challenging. Based on the lean gym leanpkg.toml I directly installed Lean 3.39.1. (When I tried the latest Lean 3 version, it complained that two_mul had nothing to do.) I also got leanproject via pipx install mathlibtools, which still worked. Prepending these imports (subsetted from minif2f_import.lean) to the proofs produced complete Lean 3 files that verified (by running lean filename.lean).

import algebra.big_operators.basic
import data.finset.basic
import data.rat.basic
import tactic

open_locale big_operators
open_locale nat
open_locale rat

I wasn't able to set up a working editor that interacted with Lean 3 to inspect the intermediate proof states, so I just printed them by inserting the tactics trace and trace_state, like so:

begin
  revert_all,
  trace "STATE 1", trace_state,
  simp [finset.sum_range_succ],
  trace "STATE 2", trace_state,
  ring,
  ...
end

Separately, prepending the additional line

set_option trace.simplify.rewrite true

(very verbose!) shows the specific actions simp performs.

appendix: bear blog sum

\displaystyle doesn't appear to work, but \sum\limits_a^b works.

The formalization sneakily introduces an $a_{0}$ term to the definition of $a_{i}$ because it's easier to start at 0 in Lean (and most other proof systems). The sums start at $k = 0$ for the same reason. But the problem is otherwise the same.↩