R08.11.01.04 · 任务小类

定理证明与形式化数学

Theorem proving & formal math

Prove statements in proof assistants.

20 条本项目编写的提案 · 分类 v1.1 · 新增基准运行 0 次。下方验证方式与部分得分规则是设计，不是执行结果。

典型应用: Lean 4 · Isabelle · Coq
小类 GUI 需求标签: CL · CLI 足够

任务提案 · 20

展开查看完整原文与建议检查方式；两种界面均保留提案英文原文。

R08.11.01.04-T01 Prove the sum of the first n odd numbers equals n squared in Lean 4

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 2 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 2 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS
应用: Coq
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 4 / 5

建议验证方式

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).

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Isabelle
交互表面: term · 终端 desk · 桌面 GUI
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 2 / 5

建议验证方式

isabelle build on a session ROOT: succeeds, no sorry/oops; lemma statements unchanged; both main proofs use 'proof (induction' structure (parsed).

建议部分得分

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

原始指令

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).

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

lake build; statement hash unchanged; no sorry/admit/native_decide; axioms limited to the standard three.

建议部分得分

20% compiles with statement; 80% proof complete

R08.11.01.04-T06 Prove prime divisibility of squares and irrationality of sqrt p in Lean

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

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.

建议部分得分

35% lemma (1); 50% lemma (2); 15% no banned lemmas

R08.11.01.04-T07 Verify a factorial loop with Hoare logic in Coq

原始指令

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.

平台: lin · Linux mac · macOS
应用: Coq
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 4 / 5

建议验证方式

coqc builds the project; framework file hashes unchanged; Print Assumptions on fact_correct is closed; theorem statement unchanged.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: mac · macOS win · Windows lin · Linux
应用: Isabelle
交互表面: desk · 桌面 GUI
GUI 需求 · 任务设定: HY · 混合
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令 click · 指向与点击
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 4 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS
应用: Coq
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

coqc succeeds; script does not contain 'decide equality'; Print Assumptions closed; lookup_correct statement unchanged; extracted lookup gives correct results on 50 test cases.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

lake build; statement unchanged; proof term references Metric.tendsto_atTop (constant walker); no sorry; standard axioms only.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: long · 长流程
提案难度: 5 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Isabelle
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 4 / 5

建议验证方式

isabelle build: function defined with 'function' (not 'fun' auto termination), termination proof present, lemma proven; no sorry/oops; statement of the lemma unchanged.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS
应用: Coq
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: long · 长流程
提案难度: 5 / 5

建议验证方式

coqc builds; definitions unchanged (hash); Print Assumptions closed for progress, preservation and soundness; statements match template.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 4 / 5

建议验证方式

lake build; statement unchanged; no sorry/native_decide; standard axioms only; decide on a finite reduction is allowed if it compiles within 400000 heartbeats.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS
应用: Coq · OCaml
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: multiapp · 多应用
提案难度: 3 / 5

建议验证方式

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.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

lake build; statement hash unchanged; no sorry; standard axioms only.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Lean 4 · Mathlib
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: 未声明
提案难度: 3 / 5

建议验证方式

lake build; statement unchanged; constant-usage walker rejects banned lemmas; no sorry; standard axioms only.

建议部分得分

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

原始指令

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.

平台: lin · Linux mac · macOS win · Windows
应用: Isabelle
交互表面: term · 终端
GUI 需求 · 任务设定: CL · CLI 足够
GUI 需求 · 普通权限: CL · CLI 足够
交互原语: code · 代码与命令
工作产物: WP06 · 代码 / 工程
条件: long · 长流程
提案难度: 5 / 5

建议验证方式

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.

建议部分得分

15% instrumented equals plain; 25% sorted; 20% permutation; 40% comparison bound

已有研究映射

以下沿用研究目录中的基准与小类映射，不是逐题标注、执行记录或产品背书。

定理证明与形式化数学

任务提案 · 20

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

原始指令

建议验证方式

建议部分得分

已有研究映射

同工作流族的小类