Theorem proving & formal math
Prove statements in proof assistants.
20 project-authored proposals · taxonomy v1.1 · 0 new benchmark runs. Verifiers and partial-credit rules below are designs, not executed results.
- Typical applications
- Lean 4 · Isabelle · Coq
- Class GUI-need label
CL· CLI-sufficient
Task proposals · 20
Expand to inspect the complete original wording and proposed checks. Original proposal text remains English in both interfaces.
R08.11.01.04-T01 Prove the sum of the first n odd numbers equals n squared in Lean 4
Original instruction
In the Lake project input/oddsum/ (Lean 4 + pinned Mathlib), file OddSum.lean states theorem odd_sum (n : Nat) : (Finset.range n).sum (fun i => 2*i+1) = n^2 := by sorry. Replace sorry with a complete proof. Do not change the statement or imports.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 2 / 5
Proposed verifier
Checker runs lake build in a clean container with the pinned toolchain; statement text hash unchanged; no sorry/admit; #print axioms shows only propext, Classical.choice, Quot.sound.
Proposed partial credit
20% file compiles with statement unchanged; 80% complete proof with clean axioms
R08.11.01.04-T02 Fill five list-lemma sorries in Lean 4
Original instruction
input/listlemmas/ListLemmas.lean defines a custom MyList type with append, reverse and length and states 5 lemmas (append_nil, append_assoc, length_append, reverse_append, reverse_reverse) with sorry. Prove all five without using Mathlib or changing definitions and statements.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 2 / 5
Proposed verifier
lake build with core Lean only (no Mathlib import allowed, checked by import list); statements and definitions byte-identical; per-lemma check that each theorem compiles without sorry.
Proposed partial credit
40% append_nil and append_assoc; 40% length_append and reverse_append; 20% reverse_reverse (equal share per lemma)
R08.11.01.04-T03 Prove BST insertion preserves the search-tree invariant in Coq
Original instruction
input/bst/BST.v defines binary trees over nat, a predicate BST via ForallT bounds, and insert. Prove insert_BST : forall t k, BST t -> BST (insert k t), plus insert_contains : forall t k, In_tree k (insert k t). Helper lemmas allowed; definitions fixed.
- Platforms
lin· Linuxmac· macOS- Applications
- Coq
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 4 / 5
Proposed verifier
coqc with pinned Coq version in clean container; Print Assumptions on both theorems reports 'Closed under the global context'; definitions unchanged (hash of the Definition/Fixpoint blocks).
Proposed partial credit
15% compiles with fixed definitions; 25% helper bound lemma; 40% insert_BST; 20% insert_contains
R08.11.01.04-T04 Prove append associativity and rev-rev in Isabelle/HOL Isar style
Original instruction
input/Lists.thy defines app and rev' on a custom list datatype. Prove app_assoc and rev_rev (rev' (rev' xs) = xs) using structured Isar proofs (proof (induction ...) ... qed) rather than single apply-scripts, adding needed helper lemmas.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Isabelle
- Interfaces
term· Terminaldesk· Desktop GUI- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 2 / 5
Proposed verifier
isabelle build on a session ROOT: succeeds, no sorry/oops; lemma statements unchanged; both main proofs use 'proof (induction' structure (parsed).
Proposed partial credit
40% app_assoc; 40% rev_rev with helpers; 20% Isar structure
R08.11.01.04-T05 Prove a symmetric inequality for positive reals in Lean 4
Original instruction
In input/ineq/Ineq.lean prove: theorem ab_bc_ca (a b c : Real) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : a + b + c = 3) : a*b + b*c + c*a <= 3. Statement and imports fixed (Mathlib pinned).
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
lake build; statement hash unchanged; no sorry/admit/native_decide; axioms limited to the standard three.
Proposed partial credit
20% compiles with statement; 80% proof complete
R08.11.01.04-T06 Prove prime divisibility of squares and irrationality of sqrt p in Lean
Original instruction
input/irrational/Sqrt.lean states (1) prime_dvd_of_dvd_sq : p.Prime -> p ∣ a^2 -> p ∣ a for naturals, and (2) irrational_sqrt_prime : p.Prime -> Irrational (Real.sqrt p). Prove both; Mathlib's Nat.Prime.irrational_sqrt and irrational_sqrt_of_* lemmas are banned.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
lake build; statements unchanged; checker scans the elaborated proof term dependencies (#print axioms plus a constant-usage walker) and fails if any banned lemma appears.
Proposed partial credit
35% lemma (1); 50% lemma (2); 15% no banned lemmas
R08.11.01.04-T07 Verify a factorial loop with Hoare logic in Coq
Original instruction
input/imp/ contains a Software-Foundations-style Imp language with Hoare rules proven sound. Prove the Hoare triple {{X = m}} fact_prog {{Y = fact m}} for the given while-loop program, choosing the loop invariant yourself. Do not modify the framework files.
- Platforms
lin· Linuxmac· macOS- Applications
- Coq
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 4 / 5
Proposed verifier
coqc builds the project; framework file hashes unchanged; Print Assumptions on fact_correct is closed; theorem statement unchanged.
Proposed partial credit
30% invariant stated and preservation goal proven; 30% initialization/exit; 40% full triple
R08.11.01.04-T08 Repair Lean proofs broken by a Mathlib version bump
Original instruction
input/algebra_lib/ builds on an older Mathlib; after bumping lakefile to the new pinned Mathlib, 12 lemmas fail (renamed lemmas, changed simp normal forms, deprecated tactics). Fix the proofs so lake build passes on the new version without changing any statement.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
lake build with new Mathlib succeeds; all theorem statements identical (elaborated type comparison against old build); no sorry; no new axioms or set_option maxHeartbeats above 400000.
Proposed partial credit
96% lemmas fixed (12, equal share each); 4% build clean with no heartbeat abuse
R08.11.01.04-T09 Prove six lemmas with Sledgehammer in Isabelle/jEdit
Original instruction
Open input/NumTheory.thy in Isabelle/jEdit. Six lemmas about gcd, divisibility and parity are stated with sorry. Use Sledgehammer and the output panel to find proofs, paste the generated proof methods, and make the theory check without sorry.
- Platforms
mac· macOSwin· Windowslin· Linux- Applications
- Isabelle
- Interfaces
desk· Desktop GUI- GUI need · task setting
HY· Hybrid- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commandsclick· Point & click- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
isabelle build of the theory: succeeds without sorry/oops; statements unchanged; proof methods of the form by (metis ...)/by (smt ...)/by auto accepted within a 30 s per-lemma timeout.
Proposed partial credit
96% six lemmas proven (equal share each); 4% theory builds clean
R08.11.01.04-T10 Define merge sort in Lean 4 and prove it sorts and permutes
Original instruction
In input/msort/MSort.lean implement msort : List Nat -> List Nat by merge sort with well-founded recursion and prove msort_sorted : List.Sorted (· ≤ ·) (msort l) and msort_perm : msort l ~ l. Using List.mergeSort or its lemmas is banned.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 4 / 5
Proposed verifier
lake build; theorem statements match the template; banned-constant walker finds no List.mergeSort*; checker also evaluates msort on 1000 random lists against List.insertionSort.
Proposed partial credit
20% msort defined and terminating; 10% evaluates correctly; 35% perm proof; 35% sorted proof
R08.11.01.04-T11 Prove decidable equality and a correct lookup function in Coq
Original instruction
input/colors/Colors.v defines an inductive type of RGB-like colors with 6 constructors (two with nat arguments). Define color_eq_dec : forall x y : color, {x = y} + {x <> y} without the 'decide equality' tactic, use it to implement lookup on association lists, and prove lookup_correct as stated.
- Platforms
lin· Linuxmac· macOS- Applications
- Coq
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
coqc succeeds; script does not contain 'decide equality'; Print Assumptions closed; lookup_correct statement unchanged; extracted lookup gives correct results on 50 test cases.
Proposed partial credit
40% decidable equality; 20% lookup implementation; 40% lookup_correct
R08.11.01.04-T12 Prove a sequence converges using the epsilon-N definition in Lean
Original instruction
In input/analysis/Conv.lean prove theorem conv : Filter.Tendsto (fun n : Nat => (2*n + 1 : Real) / (n + 3)) Filter.atTop (nhds 2) using Metric.tendsto_atTop (an explicit epsilon-N argument). Statement fixed.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
lake build; statement unchanged; proof term references Metric.tendsto_atTop (constant walker); no sorry; standard axioms only.
Proposed partial credit
20% reduces to epsilon-N goal; 30% chooses valid N; 50% complete proof
R08.11.01.04-T13 Formally prove a Putnam algebra problem in Lean 4
Original instruction
input/putnam/Problem.lean contains a formal statement of a Putnam A-section problem on a functional equation over the reals (the answer is fixed in the statement). Prove it. Imports are Mathlib only; statement fixed.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
long· Long-horizon- Proposed difficulty
- 5 / 5
Proposed verifier
lake build in clean container; statement hash unchanged; no sorry/admit/native_decide; standard axioms only. Intermediate lemmas may be added and are credited if they appear in the reference proof sketch list.
Proposed partial credit
15% compiles; 45% three key intermediate lemmas from sketch (equal shares); 40% complete proof
R08.11.01.04-T14 Prove termination with a custom measure in Isabelle's function package
Original instruction
input/Collatzish.thy defines a function f on pairs of naturals that decreases a lexicographic combination only. State it with the function package, prove termination with an explicit measure (relation ...), and prove the stated lemma that f always returns a value <= the first argument.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Isabelle
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 4 / 5
Proposed verifier
isabelle build: function defined with 'function' (not 'fun' auto termination), termination proof present, lemma proven; no sorry/oops; statement of the lemma unchanged.
Proposed partial credit
20% function defined; 45% termination proof; 35% correctness lemma
R08.11.01.04-T15 Prove progress and preservation for a typed arithmetic language in Coq
Original instruction
input/tyarith/ defines terms (booleans, nats, if, succ, pred, iszero), a small-step relation and typing. Prove progress (well-typed terms are values or step) and preservation (typing is preserved by steps), then type soundness for multi-step reduction.
- Platforms
lin· Linuxmac· macOS- Applications
- Coq
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
long· Long-horizon- Proposed difficulty
- 5 / 5
Proposed verifier
coqc builds; definitions unchanged (hash); Print Assumptions closed for progress, preservation and soundness; statements match template.
Proposed partial credit
15% canonical-forms lemmas; 35% progress; 35% preservation; 15% soundness
R08.11.01.04-T16 Prove that among any five integers three sum to a multiple of 3
Original instruction
In input/egz/EGZ3.lean prove: theorem three_of_five (f : Fin 5 -> Int) : ∃ i j k, i < j ∧ j < k ∧ (3 : Int) ∣ f i + f j + f k. Mathlib pinned; statement fixed.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 4 / 5
Proposed verifier
lake build; statement unchanged; no sorry/native_decide; standard axioms only; decide on a finite reduction is allowed if it compiles within 400000 heartbeats.
Proposed partial credit
25% reduction to residues mod 3; 25% case split structure; 50% complete proof
R08.11.01.04-T17 Prove a Coq sorting function correct and extract it to OCaml
Original instruction
input/isort/ISort.v defines insertion sort on nat lists. Prove sorted_isort and Permutation l (isort l), then extract isort to OCaml (output/isort.ml) and build output/main.ml that sorts the integers in input/test.txt.
- Platforms
lin· Linuxmac· macOS- Applications
- Coq · OCaml
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
multiapp· Multi-app- Proposed difficulty
- 3 / 5
Proposed verifier
coqc builds with closed assumptions; extracted isort.ml is generated by Extraction (header check); ocamlfind build succeeds and output on test.txt and 3 hidden files equals sorted reference.
Proposed partial credit
35% sorted proof; 35% permutation proof; 30% extraction builds and runs correctly
R08.11.01.04-T18 Prove a group with all squares trivial is abelian in Lean
Original instruction
In input/groups/Boolean.lean prove: theorem comm_of_sq_one {G : Type*} [Group G] (h : ∀ g : G, g * g = 1) : ∀ a b : G, a * b = b * a. Statement fixed; Mathlib pinned.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
lake build; statement hash unchanged; no sorry; standard axioms only.
Proposed partial credit
30% derives inverse equals self; 70% complete commutativity proof
R08.11.01.04-T19 Prove trace(AB) = trace(BA) without the library lemma in Lean
Original instruction
In input/linalg/Trace.lean prove theorem my_trace_mul_comm {n R : Type*} [Fintype n] [CommRing R] (A B : Matrix n n R) : Matrix.trace (A * B) = Matrix.trace (B * A). Matrix.trace_mul_comm and trace_mul_cycle lemmas are banned.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Lean 4 · Mathlib
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
- None declared
- Proposed difficulty
- 3 / 5
Proposed verifier
lake build; statement unchanged; constant-usage walker rejects banned lemmas; no sorry; standard axioms only.
Proposed partial credit
30% unfolds trace and matrix product into double sums; 70% complete proof without banned lemmas
R08.11.01.04-T20 Prove insertion sort correct with a quadratic comparison bound in Isabelle
Original instruction
input/ISortCost.thy defines insertion sort and an instrumented version returning (result, comparisons). Prove the instrumented result equals the plain sort, that the output is sorted and a permutation (mset), and that comparisons <= n*(n-1)/2 for inputs of length n.
- Platforms
lin· Linuxmac· macOSwin· Windows- Applications
- Isabelle
- Interfaces
term· Terminal- GUI need · task setting
CL· CLI-sufficient- GUI need · ordinary access
CL· CLI-sufficient- Interaction primitives
code· Code & commands- Work product
WP06· Code/engineering- Conditions
long· Long-horizon- Proposed difficulty
- 5 / 5
Proposed verifier
isabelle build succeeds without sorry/oops; the 4 stated theorems unchanged and proven; checker also evaluates the instrumented function on 100 random lists to confirm the bound is tight for reversed input.
Proposed partial credit
15% instrumented equals plain; 25% sorted; 20% permutation; 40% comparison bound
Mapped research references
Existing benchmark-to-class links from the research catalog. They are not record-level annotations, executions or product endorsements.