Numina & Kimi Team
Figure 1: Performance comparison of theorem proving models on the miniF2F-test dataset.
We’re excited to announce the discharge of Kimina-Prover-72B, our state-of-the-art theorem proving model trained with the Kimi k1.5[1] RL pipeline based on Qwen2.5-72B [2]. Alongside it, we’re also releasing two distilled variants: Kimina-Prover-Distill-8B and 1.7B (based on Qwen3-8B and Qwen3-1.7B[3] respectively).
Our key innovations include:
-
Test-Time Reinforcement Learning Search: A trainable agentic proving framework that allows the model to recursively discover, mix and apply multiple lemmas to construct complex proofs, constructing on a novel lemma-enabled pattern.
-
Error-Fixing Capability: Kimina-Prover can read and interpret Lean’s error messages and propose targeted fixes, demonstrating significantly higher sample efficiency in comparison with regenerating proofs from scratch.
These advancements enable Kimina-Prover to resolve difficult mathematical problems and surpass prior methods. As shown in Figure 1, on the widely used miniF2F benchmark, Kimina-Prover achieves a state-of-the-art pass rate of 92.2%.
We deal with automated theorem proving (ATP) within the Lean 4 language, aiming to automate the development of formal mathematical proofs. Recent advances in neural theorem proving have significantly improved the flexibility of AI systems to help with or automate this process. Notable progress includes AlphaProof[4] from Google DeepMind, which demonstrated strong performance on problems at the extent of the International Mathematical Olympiad. Open-source systems akin to DeepSeek-Prover-V2[5], which contains reinforcement learning, have also achieved state-of-the-art results. As well as, neuro-symbolic agentic approaches like DSP+[6] have shown that competitive performance is feasible without large-scale training by leveraging off-the-shelf models in a modular framework.
Our earlier work of Kimina-Prover Preview[7] introduced a big language model for formal theorem proving in Lean, establishing a brand new performance baseline on the miniF2F benchmark. Trained with a large-scale reinforcement learning pipeline, the model adopted a reasoning-driven exploration paradigm and demonstrated that larger models can function stronger formal reasoners. Its structured reasoning pattern enabled efficient proof search and emulated human-like problem-solving strategies.
Following this initial success, we continued to enhance the model through further iterations of reinforcement learning. Nevertheless, single-step reasoning stays insufficient for solving complex problems that require long, multi-stage proofs. To handle this limitation, we introduce the Test-Time Reinforcement Learning (TTRL) search framework, which enables the model to find, mix, and reuse multiple intermediate lemmas autonomously. This framework supports deeper, long-horizon reasoning by decomposing hard problems into reusable subcomponents.
A key ingredient of TTRL search is the lemma-enabled pattern, which allows the model to discover and apply intermediate lemmas as a part of its proof construction process. This structured reuse of intermediate results significantly expands the model’s problem-solving capability beyond single-step generation.
To further enhance robustness, we also integrate an error-fixing mechanism that interprets Lean’s error messages and proposes targeted corrections. This permits the model to refine its outputs through iterative feedback, improving proof reliability and overall sample efficiency.
A Latest State-of-the-Art
| Model | pass@1 | pass@32 | pass@1024 |
|---|---|---|---|
| Kimina-Prover-1.7B | 46.7 | 73.4 | — |
| DSP+ | 52.5 | 71.3 | 80.7 |
| DeepSeek-Prover-V2-7B | 58.6 | 75.6 | 79.9 |
| Kimina-Prover-8B | 61.1 | 78.3 | — |
| DeepSeek-Prover-V2-671B | 61.9 | 82.4 | 86.6 |
| Kimina-Prover-72B | 63.9 | 84.0 | 87.7 |
Table 1: Performance comparison of theorem proving models on the miniF2F-test dataset under equivalent sampling budgets. Kimina-Prover-72B achieves state-of-the-art performance across all evaluated settings.
As the mix of the proposed techniques leads to significant improvements in formal theorem proving performance. On the miniF2F benchmark, Kimina-Prover achieves a pass rate of 84.0% with pass@32 and 86.4% with the addition of a single round of error correction. With pass@1024, the pass rate reaches 87.7%. Applying the complete Test-Time Reinforcement Learning (TTRL) search framework yields a final pass rate of 92.2%, with an estimated pass upper sure of roughly 42,000. Nevertheless, this pass budget could be substantially optimized in future versions, as a big portion of the present sampling is spent on proving unhelpful or redundant lemmas.
Notably, these results indicate a shift within the scaling behavior of the prover. While earlier versions exhibited roughly linear improvements in log scale with increasing sampling budget, the present system shows diminishing returns beyond pass@1024. This means that further gains are less depending on increased sampling and as an alternative require more sophisticated search strategies, akin to those introduced by TTRL.
Lemma enabled pattern
The lemma-enabled pattern is designed to equip the model with the flexibility to discover and utilize useful lemmas provided within the input. To support this capability, during reinforcement learning (RL) training, a random subset of 1 to a few formal lemmas is prepended to the issue context, exposing the prover to potentially useful intermediate results that may aid in constructing the ultimate proof. These lemmas are prepared through a two-step pipeline: (1) a general-purpose LLM generates candidate lemmas in natural language; (2) these are then translated into formal statements using our Kimina-Autoformalizer-7b.
Initial observations showed that the model had a low tendency to include the provided lemmas. To handle this, we introduced a preference-based reward shaping strategy throughout the RL framework. When a theorem could possibly be proven through multiple trajectories, solutions that successfully leveraged a provided lemma were assigned a better reward, while people who didn’t were penalized. This approach proved effective, increasing the lemma utilization rate to a stable 30–40% after training. Importantly, this method not only encouraged lemma usage but additionally promoted selectivity: the model learned to use lemmas strategically after they were useful, while ignoring irrelevant ones, demonstrating more efficient and human-like reasoning behavior.
TTRL search
Figure 2: Diagram of the Test-Time Reinforcement Learning (TTRL) Search framework. It consists of three principal components: RL training, sublemma generation, and negation filtering. Sublemmas are generated and formalized, then integrated into the training loop with dynamic scoring and pruning. A negation filter ensures logical consistency by discarding invalid lemmas.
The lemma-enabled pattern allowed the model to include pre-generated lemmas as intermediate steps in constructing proofs. Nevertheless, we observed that randomly sampling and inserting lemmas was insufficient for solving complex problems requiring highly structured and deeply nested reasoning. To handle this limitation, we developed the Test-Time Reinforcement Learning Search framework—a trainable, agentic approach that systematically organizes, filters, and composes a big set of candidate lemmas to construct complete proofs. This framework transitions the method from random exploration to a more strategic, goal-directed search.
As illustrated in Figure 2, we define the search scope of every problem as the issue itself together with its associated candidate lemmas. TTRL Search tracks a lemma utilization rating inside each search scope to measure how ceaselessly and effectively each lemma contributes to the ultimate proof. In the beginning of every RL training iteration, for every problem (i.e., search scope), we construct K = 10 input variants by prepending different mixtures of lemmas. To balance exploration and exploitation, 60% of the inputs are built using the top-ranking lemmas—those with the very best utilization scores—focusing the model on essentially the most promising proof paths. The remaining 40% are formed by including these top lemmas alongside one to 4 randomly chosen additional lemmas, encouraging exploration of novel and potentially useful lemma mixtures.
To make sure quality, a filtering mechanism prunes lemmas that consistently fail to contribute meaningfully: any lemma that fails to attain a utilization rating of a minimum of τ=0.10 after 50 insertion attempts is faraway from the search pool.
A key feature of TTRL is its recursive search mechanism. The search scope will not be limited to the unique theorem but can be maintained for every lemma, allowing the framework to recursively decompose the issue into smaller subproblems. A parallel sublemma generation process runs throughout, and at any time when a theorem or lemma fails to search out a proof after N = 128 attempts, latest candidate sublemmas are generated. This recursive strategy enables test-time scaling of reasoning depth, significantly extending the model’s effective problem-solving capability.
To take care of logical soundness, we address a failure mode wherein incorrectly formalized lemmas may lead to trivial or invalid proofs. In such cases, the model may exploit inconsistencies to construct seemingly valid but unsound solutions. To forestall this, we introduce a negation proving process: for every newly generated lemma, we try to prove its logical negation. If the negated statement is provable, it indicates that the unique lemma is logically inconsistent and is straight away discarded. This step ensures the reliability and soundness of the general proof construction process.
Enabling Error-Fixing in Kimina-Prover
A critical limitation of recent advanced theorem proving models is their lack of the flexibility to correct proofs based on feedback from the proof assistant—capabilities that human users routinely leverage. To handle this gap, we developed a dedicated framework to integrate error-fixing capabilities into Kimina-Prover.
SFT Data Generation for Error Correction. General-purpose large language models exhibit a low success rate when interpreting Lean’s error messages and proposing valid corrections. To beat this, we constructed a specialized Supervised Nice-Tuning (SFT) dataset tailored for error correction. This dataset consists of triplets in the shape of (incorrect proof, Lean feedback, correct proof). To complement the supervision signal, we prompted Claude 3.7 sonnet[8] to synthesize step-by-step reasoning chains explaining how the inaccurate proof could be transformed into the proper one using the provided feedback. The result’s a high-quality dataset that features not only the initial and corrected proofs but additionally the intermediate reasoning, facilitating more practical learning.
Batched Failure Replay Strategy. Integrating error correction directly into the reinforcement learning (RL) loop initially proved ineffective as a consequence of the low success rate (~1%) of the SFT model in fixing errors, leading to sparse rewards and unstable training. To handle this, we designed the Batched Failure Replay strategy. Relatively than attempting to correct errors immediately during an RL iteration, all failed proof attempts from iteration N are collected. In the following iteration N+1, the training batch consists of a fixed-size union of those prior failures (e.g., 500 samples) and standard problems from the prompt set (e.g., one other 500 samples). This ensures consistent and high-volume exposure to error correction tasks in each training step, enabling the model to step by step learn effective error-handling behaviors in a stable and data-efficient manner.
| 16+16 attempt-and-fix | 32×1 brute-force | 32+32 attempt-and-fix | |
|---|---|---|---|
| kimina-prover | 35.6 | 28.8 | 44.1 |
Table 2: Performance comparison between error-fixing and brute-force strategies on a particular subset of 59 MiniF2F-Test problems with the bottom win rates. Under equal sample budgets, the error-fixing strategies (16+16) outperform the brute-force baseline (32×1), demonstrating improved sample efficiency.
This training approach led to measurable improvements within the model’s ability to get better from failure. The model advanced from correcting basic syntax errors to resolving complex logical mistakes and, eventually, discovering alternative proof strategies when initial attempts failed. Crucially, this capability improved sample efficiency. As shown in Table 2, we compared different strategies under fixed computational budgets. The 16+16 attempt-and-fix strategy—consisting of 16 initial proof attempts, each followed by one error-fixing attempt—achieved a hit rate of 35.6%, outperforming the 32×1 brute-force baseline, which reached 28.8% with 32 independent attempts. Further increasing the sample budget to 32+32 with error correction yielded a hit rate of 44.1%. These results show that enabling the model to correct its own errors is a more efficient use of computational resources than repeated trial-and-error.
Other improvement
Along with our core TTRL search and Error fixing, we developed several other novel techniques to reinforce the model’s learning process and problem-solving capabilities.
Prompt Set Curation and Iteration. Effective data curation is critical for reinforcement learning (RL) efficiency. Our initial prompt set of over 300K problems was refined to a competition-focused subset of roughly 90K, with an emphasis on problems from sources akin to the olympiads-ref subset of NuminaMath 1.5[9]. During RL, we applied dynamic filtering: problems with consistently high success rates were removed to take care of challenge, while persistently difficult problems were decomposed into simpler subproblems or variations using a general-purpose LLM. The ultimate prompt set combines auto-formalized statements for broad coverage, human-annotated problems for quality, and augmented variations for targeted skill development. The curated prompt set might be open-sourced.
Continuous Pre-training on Lean Data. To handle the limited Lean proficiency in most base models, we applied Continuous Pre-training (CPT). A 6-billion-token CPT dataset was constructed from multiple sources: 260M tokens from online platforms akin to GitHub, 5.5B tokens of compiler-validated rollout data from our RL pipeline, and extra structured data in state–tactic–state and state–tactic–error formats to reinforce diversity. These structured data supplements the bottom model with additional domain knowledge.
Random Proof Cut Data Augmentation. To higher utilize high-quality, human-annotated proofs that lack intermediate reasoning steps, we developed the Random Proof Cut technique. This method augments such data using two variations:
- Proof truncation: The ultimate a part of a proof is removed, and the model must complete it.
- Proof infilling: A randomly chosen internal block is replaced with the placeholder token
sorry, and the model must reconstruct the missing steps.
This strategy allows the model to learn tips on how to extend existing lines of reasoning and to fill in logical gaps, effectively integrating human-generated content into the training process.
Non-proof Problem Solving. Many problems are presented in the shape of requiring a final answer, which can’t be naturally framed as a conventional proof task. Inspired by the CombiBench[10] evaluation methodology, we introduced a capability for non-proof problem solving to unify answer generation with proof construction. On this setting, the model is given an issue with the ultimate answer field left blank. It performs a two-stage process inside a single inference: it first deduces the proper answer after which generates a whole formal proof to justify that answer. This approach ensures the model’s reasoning is explicitly conditioned on reaching the proper solution.
Here we offer some proof cases found by our newest Kimina-prover model. The whole list of solved miniF2F problems is obtainable on GitHub
TTRL search proof example
The system recursively decomposed the issue into 4 layers of lemmas using a TTRL search approach, ultimately generating a 520-line formal proof. During this recursive proving process, initially, just one lemma, sum_cexp_div_pow_ne_zero, remained to be solved. While this conclusion seems straightforward to prove informally, it could still require quite a lot of steps to prove it rigorously in Lean 4. Our system recursively generated two extra layers of lemmas and obtained a 260-line formal proof for sum_cexp_div_pow_ne_zero. This proof is valid under Mathlib v4.15
Sample proof for imo 1969 p2
Proof structure
Figure 3: Proof dependency graph for the theory imo_1969_p2, illustrating the structure of lemma references and calls. Each node represents a lemma or theorem, with directed edges indicating dependency relationships (i.e., one lemma calling one other). Lemma names are randomly generated during proof construction; for clarity, we manually renamed them post hoc to reflect their mathematical content more accurately.
Formal code
import Mathlib
open Finset in
theorem norm_le_sum_norm_of_sum_eq_zero {N : ℕ} (hN : N > 0) (z : ℕ → ℂ)
(hsum : ∑ i ∈ range N, z i = 0) :
‖z 0‖ ≤ ∑ i ∈ Icc 1 (N - 1), ‖z i‖ := by
by_cases h : N > 1
·
have h6 : ∑ i in range N, z i = z 0 + ∑ i in Icc 1 (N - 1), z i := by
have h10 : range N = {0} ∪ Icc 1 (N - 1) := by
ext x
simp
omega
rw [h10]
rw [sum_union]
·
simp
·
apply disjoint_left.mpr
intro x hx1 hx2
simp at hx1
simp [hx1] at hx2
have h3 : z 0 = - (∑ i ∈ Icc 1 (N - 1), z i) := by
have h4 : ∑ i in range N, z i = 0 := hsum
rw [h6] at h4
calc
z 0 = (z 0 + ∑ i in Icc 1 (N - 1), z i) - ∑ i in Icc 1 (N - 1), z i := by ring
_ = (0 : ℂ) - ∑ i in Icc 1 (N - 1), z i := by rw [h4]
_ = - (∑ i in Icc 1 (N - 1), z i) := by ring
have h11 : ‖z 0‖ = ‖(∑ i ∈ Icc 1 (N - 1), z i : ℂ)‖ := by
rw [h3]
simp [norm_neg]
have h12 : ‖(∑ i ∈ Icc 1 (N - 1), z i : ℂ)‖ ≤ ∑ i ∈ Icc 1 (N - 1), ‖z i‖ := by
apply norm_sum_le
linarith [h11, h12]
·
have h5 : N = 1 := by
omega
rw [h5]
have h6 : ∑ i in range 1, z i = 0 := by
have h7 : N = 1 := h5
have h8 : ∑ i in range N, z i = 0 := hsum
rw [show N = 1 by omega] at h8
simpa using h8
have h7 : z 0 = 0 := by
simp at h6
all_goals
try tauto
rw [show z 0 = (0 : ℂ) by exact h7]
simp
open Finset in
theorem sum_pow_one_half_from_two_to_N {N : ℕ} (hN : 0 < N) :
∑ j ∈ Icc 1 (N - 1), (1 / 2 : ℝ) ^ (j + 1) = 1 / 2 - 1 / 2 ^ N := by
have h2 : ∀ (k : ℕ), ∑ j in Icc 1 (k), (1 / 2 : ℝ) ^ (j + 1) = 1 / 2 - 1 / 2 ^ (k + 1 : ℕ) := by
intro k
induction k with
| zero =>
simp
| succ k ihk =>
rw [sum_Icc_succ_top (by linarith)]
rw [ihk]
field_simp at *
ring_nf
have h4 : ∑ j in Icc 1 (N - 1), (1 / 2 : ℝ) ^ (j + 1) = 1 / 2 - 1 / 2 ^ (N : ℕ) := by
have h5 : ∑ j in Icc 1 (N - 1), (1 / 2 : ℝ) ^ (j + 1) = 1 / 2 - 1 / 2 ^ ((N - 1 : ℕ) + 1 : ℕ) := by
apply h2 (N - 1)
rw [h5]
have h6 : (N - 1 : ℕ) + 1 = N := by
omega
rw [h6]
exact h4
open Complex Finset in
theorem sum_eq_zero_of_sq_add_sq_eq_geom_seq_false {N : ℕ} (hN : 0 < N) (x y : Fin N → ℝ)
(hxsum : ∑ i : Fin N, x i = 0) (hysum : ∑ i : Fin N, y i = 0)
(hxy : ∀ j : Fin N, (x j)^2 + (y j)^2 = (1/4)^(j.1+1)) :
False := by
let z : ℕ → ℂ := fun i => if h : i < N then (x ⟨i, h⟩ : ℂ) + (y ⟨i, h⟩ : ℂ) * I else 0
have hsumz : ∑ i in range N, z i = 0 := by
have h4 : ∑ i in range N, z i = (∑ i : Fin N, ((x i : ℂ) + (y i : ℂ) * I)) := by
simp [z, Finset.sum_fin_eq_sum_range, Finset.sum_congr]
rw [h4]
simp [Complex.ext_iff, Finset.sum_congr, hxsum, hysum]
have hz0 : ‖z 0‖ ≤ ∑ i ∈ Icc 1 (N - 1), ‖z i‖ := norm_le_sum_norm_of_sum_eq_zero hN z hsumz
have h2 : ‖z 0‖ = (1 / 2 : ℝ) := by
have h6 : z 0 = (x ⟨0, by omega⟩ : ℂ) + (y ⟨0, by omega⟩ : ℂ) * I := by
have h7 : (0 : ℕ) < N := by omega
simp [z, h7]
rw [h6]
have h7 : ((x ⟨0, by omega⟩ : ℝ) ^ 2 + (y ⟨0, by omega⟩ : ℝ) ^ 2) = (1 / 4 : ℝ) := by
have h8 := hxy (⟨0, by omega⟩)
norm_num at h8 ⊢
nlinarith
have h8 : ‖((x ⟨0, by omega⟩ : ℂ) + (y ⟨0, by omega⟩ : ℂ) * I)‖ = Real.sqrt ((x ⟨0, by omega⟩ : ℝ) ^ 2 + (y ⟨0, by omega⟩ : ℝ) ^ 2) := by
simp [Complex.norm_eq_abs, Complex.abs, Complex.normSq]
all_goals
ring_nf
rw [h8, h7]
have h9 : Real.sqrt ((1 / 4 : ℝ)) = (1 / 2 : ℝ) := by
rw [Real.sqrt_eq_iff_mul_self_eq] <;> norm_num
rw [h9]
have h3 : ∑ i ∈ Icc 1 (N - 1), ‖z i‖ = ∑ i ∈ Icc 1 (N - 1), (1 / 2 : ℝ) ^ (i + 1 : ℕ) := by
apply Finset.sum_congr
.
rfl
.
intro i hi
have h10 : i ≥ 1 := by
have h11 : i ∈ Icc (1 : ℕ) (N - 1) := by
simpa using hi
simp at h11 ⊢
omega
have h11 : i ≤ N - 1 := by
have h12 : i ∈ Icc (1 : ℕ) (N - 1) := by
simpa using hi
simp at h12 ⊢
omega
have h12 : i < N := by
omega
have h13 : z i = (x ⟨i, by omega⟩ : ℂ) + (y ⟨i, by omega⟩ : ℂ) * I := by
have h14 : i < N := by omega
simp [z, h14]
have h14 : ‖z i‖ = (1 / 2 : ℝ) ^ (i + 1 : ℕ) := by
rw [h13]
have h14 : ((x ⟨i, by omega⟩ : ℝ) ^ 2 + (y ⟨i, by omega⟩ : ℝ) ^ 2) = (1 / 4 : ℝ) ^ (i + 1 : ℕ) := by
have h15 := hxy (⟨i, by omega⟩)
norm_num at h15 ⊢
nlinarith
have h15 : ‖((x ⟨i, by omega⟩ : ℂ) + (y ⟨i, by omega⟩ : ℂ) * I)‖ = Real.sqrt ((x ⟨i, by omega⟩ : ℝ) ^ 2 + (y ⟨i, by omega⟩ : ℝ) ^ 2) := by
simp [Complex.norm_eq_abs, Complex.abs, Complex.normSq]
all_goals
ring_nf
rw [h15]
have h16 : Real.sqrt ((x ⟨i, by omega⟩ : ℝ) ^ 2 + (y ⟨i, by omega⟩ : ℝ) ^ 2) = (1 / 2 : ℝ) ^ (i + 1 : ℕ) := by
have h17 : ((x ⟨i, by omega⟩ : ℝ) ^ 2 + (y ⟨i, by omega⟩ : ℝ) ^ 2) = (1 / 4 : ℝ) ^ (i + 1 : ℕ) := h14
rw [h17]
have h18 : Real.sqrt ((1 / 4 : ℝ) ^ (i + 1 : ℕ)) = (1 / 2 : ℝ) ^ (i + 1 : ℕ) := by
have h19 : ((1 / 4 : ℝ) : ℝ) = (1 / 2 : ℝ) ^ (2 : ℕ) := by norm_num
rw [h19]
have h20 : Real.sqrt (((1 / 2 : ℝ) ^ (2 : ℕ)) ^ (i + 1 : ℕ)) = (1 / 2 : ℝ) ^ (i + 1 : ℕ) := by
have h21 : ((1 / 2 : ℝ) ^ (2 : ℕ)) ^ (i + 1 : ℕ) = ((1 / 2 : ℝ) ^ (i + 1 : ℕ)) ^ 2 := by
have h22 : ((1 / 2 : ℝ) ^ (2 : ℕ)) ^ (i + 1 : ℕ) = (1 / 2 : ℝ) ^ (2 * (i + 1 : ℕ) : ℕ) := by
rw [← pow_mul]
all_goals ring_nf
have h23 : ((1 / 2 : ℝ) ^ (i + 1 : ℕ)) ^ 2 = (1 / 2 : ℝ) ^ (2 * (i + 1 : ℕ) : ℕ) := by
ring_nf
rw [h22, h23]
rw [h21]
have h22 : Real.sqrt (((1 / 2 : ℝ) ^ (i + 1 : ℕ)) ^ 2) = (1 / 2 : ℝ) ^ (i + 1 : ℕ) := by
rw [Real.sqrt_sq (show (1 / 2 : ℝ) ^ (i + 1 : ℕ) ≥ 0 by positivity)]
rw [h22]
exact h20
exact h18
exact h16
linarith
rw [h3] at hz0
rw [h2] at hz0
have h6 : ∑ i ∈ Icc 1 (N - 1), (1 / 2 : ℝ) ^ (i + 1 : ℕ) = (1 / 2 - 1 / 2 ^ N : ℝ) := by
have h7 : ∑ i ∈ Icc 1 (N - 1), (1 / 2 : ℝ) ^ (i + 1 : ℕ) = (1 / 2 - 1 / 2 ^ N : ℝ) := sum_pow_one_half_from_two_to_N hN
linarith
rw [h6] at hz0
have h7 : (1 / 2 ^ N : ℝ) > 0 := by
have h10 : (1 / 2 ^ N : ℝ) > 0 := by
have h11 : (1 / 2 ^ N : ℝ) = (1 / 2 : ℝ) ^ N := by
ring_nf
rw [h11]
positivity
linarith
have h11 : (1 / 2 - 1 / 2 ^ N : ℝ) < (1 / 2 : ℝ) := by
have h12 : (1 / 2 ^ N : ℝ) > 0 := h7
linarith
linarith
open BigOperators Real Nat Topology Rat in
theorem sum_cexp_div_pow_ne_zero {N : ℕ} (hN : N > 0) (a : Fin N → ℝ) :
((∑ j : Fin N, cos (a j) / 2 ^ (j : ℕ))^2 +
(∑ j : Fin N, sin (a j) / 2 ^ (j : ℕ))^2) > 0 := by
by_contra h
push_neg at h
have h1 : (∑ j : Fin N, cos (a j) / 2 ^ (j : ℕ)) ^ 2 ≥ 0 := by
apply sq_nonneg
have h2 : (∑ j : Fin N, sin (a j) / 2 ^ (j : ℕ)) ^ 2 ≥ 0 := by
apply sq_nonneg
have h3 : (∑ j : Fin N, cos (a j) / 2 ^ (j : ℕ)) ^ 2 = 0 := by
linarith
have h4 : (∑ j : Fin N, sin (a j) / 2 ^ (j : ℕ)) ^ 2 = 0 := by
linarith
have h5 : (∑ j : Fin N, cos (a j) / 2 ^ (j : ℕ)) = 0 := by
nlinarith
have h6 : (∑ j : Fin N, sin (a j) / 2 ^ (j : ℕ)) = 0 := by
nlinarith
let x : Fin N → ℝ := fun j => cos (a j) / 2 ^ (j.1 + 1 : ℕ)
let y : Fin N → ℝ := fun j => sin (a j) / 2 ^ (j.1 + 1 : ℕ)
have hxsum : ∑ i : Fin N, x i = 0 := by
have eq2 : ∑ i : Fin N, x i = (∑ i : Fin N, (cos (a i) / 2 ^ (i.1 : ℕ) : ℝ)) / 2 := by
have eq3 : ∑ i : Fin N, x i = ∑ i : Fin N, (cos (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ) := by
congr
rw [eq3]
have eq4 : ∑ i : Fin N, (cos (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ) = (∑ i : Fin N, (cos (a i) / 2 ^ (i.1 : ℕ) : ℝ)) / 2 := by
calc
∑ i : Fin N, (cos (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ)
= ∑ i : Fin N, ((cos (a i) / 2 ^ (i.1 : ℕ) : ℝ) / 2) := by
apply Finset.sum_congr
.
rfl
intro i hi
have h12 : (cos (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ) = (cos (a i) / 2 ^ (i.1 : ℕ) : ℝ) / 2 := by
have h11 : (2 : ℝ) ^ (i.1 + 1 : ℕ) = (2 : ℝ) ^ (i.1 : ℕ) * 2 := by
ring_nf
rw [h11]
field_simp
all_goals ring
exact h12
_ = (∑ i : Fin N, (cos (a i) / 2 ^ (i.1 : ℕ) : ℝ)) / 2 := by
simp [Finset.sum_div]
exact eq4
rw [eq2]
rw [show ∑ i : Fin N, (cos (a i) / 2 ^ (i.1 : ℕ) : ℝ) = (0 : ℝ) by simpa using h5]
all_goals norm_num
have hysum : ∑ i : Fin N, y i = 0 := by
have eq2 : ∑ i : Fin N, y i = (∑ i : Fin N, (sin (a i) / 2 ^ (i.1 : ℕ) : ℝ)) / 2 := by
have eq3 : ∑ i : Fin N, y i = ∑ i : Fin N, (sin (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ) := by
congr
rw [eq3]
have eq4 : ∑ i : Fin N, (sin (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ) = (∑ i : Fin N, (sin (a i) / 2 ^ (i.1 : ℕ) : ℝ)) / 2 := by
calc
∑ i : Fin N, (sin (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ)
= ∑ i : Fin N, ((sin (a i) / 2 ^ (i.1 : ℕ) : ℝ) / 2) := by
apply Finset.sum_congr
.
rfl
intro i hi
have h12 : (sin (a i) / 2 ^ (i.1 + 1 : ℕ) : ℝ) = (sin (a i) / 2 ^ (i.1 : ℕ) : ℝ) / 2 := by
have h11 : (2 : ℝ) ^ (i.1 + 1 : ℕ) = (2 : ℝ) ^ (i.1 : ℕ) * 2 := by
ring_nf
rw [h11]
field_simp
all_goals ring
exact h12
_ = (∑ i : Fin N, (sin (a i) / 2 ^ (i.1 : ℕ) : ℝ)) / 2 := by
simp [Finset.sum_div]
exact eq4
rw [eq2]
rw [show ∑ i : Fin N, (sin (a i) / 2 ^ (i.1 : ℕ) : ℝ) = (0 : ℝ) by simpa using h6]
all_goals norm_num
have hxy : ∀ j : Fin N, (x j) ^ 2 + (y j) ^ 2 = (1 / 4 : ℝ) ^ (j.1 + 1 : ℕ) := by
intro j
have h11 : cos (a j) ^ 2 + sin (a j) ^ 2 = 1 := by
exact Real.cos_sq_add_sin_sq (a j)
simp [x, y]
have h12 : (4 : ℝ) ^ (j.1 + 1 : ℕ) = (2 : ℝ) ^ (2 * (j.1 + 1 : ℕ)) := by
have h13 : (4 : ℝ) = (2 : ℝ) ^ (2 : ℕ) := by norm_num
rw [h13]
rw [← pow_mul]
have h13 : (2 : ℝ) ^ (2 * (j.1 + 1 : ℕ)) = ((2 : ℝ) ^ (j.1 + 1 : ℕ)) ^ 2 := by
ring_nf
field_simp [h11, h12, h13]
all_goals
ring_nf
have h12 : False := sum_eq_zero_of_sq_add_sq_eq_geom_seq_false (show 0 < N by omega) x y hxsum hysum hxy
tauto
open BigOperators Real Nat Topology Rat in
theorem mul_cos_sub_mul_sin_eq_mul_cos_add (C S : ℝ) (h : C ^ 2 + S ^ 2 ≠ 0) :
∃ R α : ℝ, R > 0 ∧ ∀ x : ℝ, C * cos x - S * sin x = R * cos (x + α) := by
have h1 : C ^ 2 + S ^ 2 > 0 := by
by_contra h2
push_neg at h2
have h3 : C ^ 2 ≥ 0 := sq_nonneg C
have h4 : S ^ 2 ≥ 0 := sq_nonneg S
have h5 : C ^ 2 + S ^ 2 = 0 := by nlinarith
tauto
have h2 : ∃ R : ℝ, R > 0 ∧ R ^ 2 = C ^ 2 + S ^ 2 := by
use Real.sqrt (C ^ 2 + S ^ 2)
constructor
· -- Show that sqrt (C^2 + S^2) > 0
apply Real.sqrt_pos.mpr
linarith
· -- Show that (sqrt (C^2 + S^2)) ^ 2 = C^2 + S^2
rw [Real.sq_sqrt]
positivity
rcases h2 with ⟨R, hR_pos, hR_sq⟩
have h12 : (C / R) ^ 2 + (S / R) ^ 2 = 1 := by
have h14 : R ≠ 0 := by linarith
have h15 : R ^ 2 = C ^ 2 + S ^ 2 := hR_sq
field_simp at *
nlinarith
have h13 : ∃ α : ℝ, Real.cos α = C / R ∧ Real.sin α = S / R := by
have h9 : (C / R) ^ 2 + (S / R) ^ 2 = 1 := h12
by_cases hC : C ≥ 0
· -- C ≥ 0
use Real.arcsin (S / R)
constructor
· -- Show cos (arcsin (S / R)) = C / R
have h14 : Real.cos (Real.arcsin (S / R)) = Real.sqrt (1 - (S / R) ^ 2) := by
rw [Real.cos_arcsin]
have h15 : Real.sqrt (1 - (S / R) ^ 2) = C / R := by
have h151 : (C / R) ^ 2 = 1 - (S / R) ^ 2 := by
linarith [h9]
have h161 : Real.sqrt (1 - (S / R) ^ 2) = Real.sqrt ((C / R) ^ 2) := by
rw [show 1 - (S / R) ^ 2 = (C / R) ^ 2 by linarith [h9]]
rw [h161]
have h171 : Real.sqrt ((C / R) ^ 2) = C / R := by
apply Real.sqrt_sq (show 0 ≤ C / R by
have h211 : R > 0 := hR_pos
apply div_nonneg
linarith
linarith
)
rw [h171]
rw [h14, h15]
· -- Show sin (arcsin (S / R)) = S / R
have h20 : -1 ≤ S / R := by
have h6 : (S / R) ^ 2 ≤ 1 := by nlinarith [h9]
nlinarith [sq_nonneg (S / R - 1), sq_nonneg (S / R + 1)]
have h21 : S / R ≤ 1 := by
have h6 : (S / R) ^ 2 ≤ 1 := by nlinarith [h9]
nlinarith [sq_nonneg (S / R - 1), sq_nonneg (S / R + 1)]
have h18 : Real.sin (Real.arcsin (S / R)) = S / R := by
apply Real.sin_arcsin
all_goals linarith
rw [h18]
· -- C < 0
have hC2 : C < (0 : ℝ) := by linarith
have hC3 : C / R < 0 := by
have hR_pos1 : R > 0 := hR_pos
apply div_neg_of_neg_of_pos hC2 (by linarith)
use Real.pi - Real.arcsin (S / R)
constructor
· -- Show cos (π - arcsin (S / R)) = C / R
have h28 : Real.cos (Real.pi - Real.arcsin (S / R)) = - Real.sqrt (1 - (S / R) ^ 2) := by
have h1 : Real.cos (Real.pi - Real.arcsin (S / R)) = - Real.cos (Real.arcsin (S / R)) := by
rw [Real.cos_pi_sub]
have h2 : Real.cos (Real.arcsin (S / R)) = Real.sqrt (1 - (S / R) ^ 2) := by
rw [Real.cos_arcsin]
rw [h1, h2]
have h29 : Real.sqrt (1 - (S / R) ^ 2) = - (C / R) := by
have h301 : (C / R) ^ 2 = 1 - (S / R) ^ 2 := by
linarith [h9]
have h311 : Real.sqrt (1 - (S / R) ^ 2) = Real.sqrt ((C / R) ^ 2) := by
rw [show 1 - (S / R) ^ 2 = (C / R) ^ 2 by linarith [h9]]
rw [h311]
have h321 : Real.sqrt ((C / R) ^ 2) = - (C / R) := by
have h331 : C / R < 0 := hC3
have : Real.sqrt ((C / R) ^ 2) = - (C / R) := by
rw [Real.sqrt_sq_eq_abs]
rw [abs_of_neg h331]
linarith
linarith
rw [h28, h29]
all_goals nlinarith
· -- Show sin (π - arcsin (S / R)) = S / R
have h30 : Real.sin (Real.pi - Real.arcsin (S / R)) = Real.sin (Real.arcsin (S / R)) := by
rw [Real.sin_pi_sub]
have h31 : Real.sin (Real.arcsin (S / R)) = S / R := by
have h20 : -1 ≤ S / R := by
have h6 : (S / R) ^ 2 ≤ 1 := by nlinarith [h9]
nlinarith [sq_nonneg (S / R - 1), sq_nonneg (S / R + 1)]
have h21 : S / R ≤ 1 := by
have h6 : (S / R) ^ 2 ≤ 1 := by nlinarith [h9]
nlinarith [sq_nonneg (S / R - 1), sq_nonneg (S / R + 1)]
apply Real.sin_arcsin
all_goals linarith
rw [h30, h31]
rcases h13 with ⟨α, h14, h15⟩
use R, α
constructor
· -- Show R > 0
linarith
· -- Show ∀ x : ℝ, C * cos x - S * sin x = R * cos (x + α)
intro x
have h21 : Real.cos (x + α) = Real.cos x * Real.cos α - Real.sin x * Real.sin α := by
rw [Real.cos_add]
have h22 : Real.cos α = C / R := by
linarith [h14]
have h23 : Real.sin α = S / R := by
linarith [h15]
calc
C * Real.cos x - S * Real.sin x
= R * (Real.cos x * (C / R) - Real.sin x * (S / R)) := by
field_simp [show R ≠ 0 by linarith]
all_goals ring
_ = R * (Real.cos x * Real.cos α - Real.sin x * Real.sin α) := by
rw [show Real.cos α = C / R by linarith [h14], show Real.sin α = S / R by linarith [h15]]
_ = R * Real.cos (x + α) := by
rw [h21]
theorem sum_cos_div_two_pow_eq_mul_cos (N : ℕ) (a : ℕ → ℝ) (hN : N > 0) :
∃ R0 α : ℝ, R0 > 0 ∧ ∀ x : ℝ, ∑ j : Fin N, Real.cos (a j + x) / 2 ^ j.1 =
(R0 : ℝ) * Real.cos (x + α) := by
have h2 : ((∑ j : Fin N, Real.cos (a j) / 2 ^ (j : ℕ)) ^ 2 + (∑ j : Fin N, Real.sin (a j) / 2 ^ (j : ℕ)) ^ 2) > 0 := by
apply sum_cexp_div_pow_ne_zero (by omega) (fun j : Fin N => a j)
have h4 : (∑ j : Fin N, Real.cos (a j) / 2 ^ (j : ℕ)) ^ 2 + (∑ j : Fin N, Real.sin (a j) / 2 ^ (j : ℕ)) ^ 2 ≠ 0 := by
linarith
have h5 : ∃ R α : ℝ, R > 0 ∧ ∀ x : ℝ, (∑ j : Fin N, Real.cos (a j) / 2 ^ (j : ℕ)) * Real.cos x - (∑ j : Fin N, Real.sin (a j) / 2 ^ (j : ℕ)) * Real.sin x = R * Real.cos (x + α) := by
apply mul_cos_sub_mul_sin_eq_mul_cos_add (∑ j : Fin N, Real.cos (a j) / 2 ^ (j : ℕ)) (∑ j : Fin N, Real.sin (a j) / 2 ^ (j : ℕ)) (by
exact h4
)
rcases h5 with ⟨R0, α, hR0_pos, h_eq⟩
use R0, α
constructor
.
exact hR0_pos
.
intro x
have h_eq2 : ∑ j : Fin N, Real.cos (a j + x) / 2 ^ j.1 = (∑ j : Fin N, Real.cos (a j) / 2 ^ (j : ℕ)) * Real.cos x - (∑ j : Fin N, Real.sin (a j) / 2 ^ (j : ℕ)) * Real.sin x := by
have h8 : ∀ j : Fin N, Real.cos (a j + x) / (2 : ℝ) ^ (j : ℕ) = (Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x) / (2 : ℝ) ^ (j : ℕ) := by
intro j
have h9 : Real.cos (a j + x) = Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x := by
rw [Real.cos_add]
rw [h9]
have h10 : ∑ j : Fin N, Real.cos (a j + x) / 2 ^ j.1 = ∑ j : Fin N, ((Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x) / (2 : ℝ) ^ (j : ℕ)) := by
apply Finset.sum_congr
.
rfl
.
intro j hj
have h9 : Real.cos (a j + x) / (2 : ℝ) ^ (j : ℕ) = (Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x) / (2 : ℝ) ^ (j : ℕ) := h8 j
simpa using h9
rw [h10]
have h11 : ∑ j : Fin N, ((Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x) / (2 : ℝ) ^ (j : ℕ)) =
(∑ j : Fin N, Real.cos (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.cos x - (∑ j : Fin N, Real.sin (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.sin x := by
have h12 : ∀ j : Fin N, ((Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x) / (2 : ℝ) ^ (j : ℕ)) =
(Real.cos (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.cos x - (Real.sin (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.sin x := by
intro j
ring_nf
calc
∑ j : Fin N, ((Real.cos (a j) * Real.cos x - Real.sin (a j) * Real.sin x) / (2 : ℝ) ^ (j : ℕ))
= ∑ j : Fin N, ((Real.cos (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.cos x - (Real.sin (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.sin x) := by
apply Finset.sum_congr
.
rfl
.
intro j hj
specialize h12 j
linarith
_ = (∑ j : Fin N, (Real.cos (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.cos x) - (∑ j : Fin N, (Real.sin (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.sin x) := by
rw [Finset.sum_sub_distrib]
_ = (∑ j : Fin N, Real.cos (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.cos x - (∑ j : Fin N, Real.sin (a j) / (2 : ℝ) ^ (j : ℕ)) * Real.sin x := by
rw [Finset.sum_mul, Finset.sum_mul]
exact h11
rw [h_eq2]
specialize h_eq x
linarith
open Real Set in
theorem sub_eq_int_mul_pi_of_cos_eq_zero :
∀ (θ₁ θ₂ : ℝ), cos θ₁ = 0 → cos θ₂ = 0 → ∃ m : ℤ, θ₂ - θ₁ = m * π := by
intro θ₁ θ₂ h₁ h₂
have h1 : ∃ k : ℤ, θ₁ = Real.pi / 2 + k * Real.pi := by
rw [Real.cos_eq_zero_iff] at h₁
rcases h₁ with ⟨k, hk⟩
use k
linarith
rcases h1 with ⟨k, hk1⟩
have h2 : ∃ l : ℤ, θ₂ = Real.pi / 2 + l * Real.pi := by
rw [Real.cos_eq_zero_iff] at h₂
rcases h₂ with ⟨l, hl⟩
use l
linarith
rcases h2 with ⟨l, hl2⟩
use l - k
rw [hl2, hk1]
field_simp at *
<;> ring_nf <;> norm_num
open BigOperators Real Nat Topology Rat in
theorem imo_1969_p2 (m n : ℝ) (k : ℕ) (a : ℕ → ℝ) (y : ℝ → ℝ) (h₀ : 0 < k)
(h₁ : ∀ x, y x = ∑ i in Finset.range k, Real.cos (a i + x) / 2 ^ i) (h₂ : y m = 0)
(h₃ : y n = 0) : ∃ t : ℤ, m - n = t * Real.pi := by
have h4 : y m = ∑ i in Finset.range k, Real.cos (a i + m) / 2 ^ i := by
specialize h₁ m
simpa using h₁
have h5 : y n = ∑ i in Finset.range k, Real.cos (a i + n) / 2 ^ i := by
specialize h₁ n
simpa using h₁
rw [h4] at h₂
rw [h5] at h₃
have h9 : ∃ R0 α : ℝ, R0 > 0 ∧ ∀ x : ℝ, ∑ j : Fin k, Real.cos (a j + x) / 2 ^ j.1 = R0 * Real.cos (x + α) := by
apply sum_cos_div_two_pow_eq_mul_cos k (fun (j : ℕ) => a j) (by omega)
rcases h9 with ⟨R0, α, hR0, h_eq3⟩
have h10 : ∑ i in Finset.range k, Real.cos (a i + m) / 2 ^ i = R0 * Real.cos (m + α) := by
have h11 : ∑ i in Finset.range k, Real.cos (a i + m) / 2 ^ i = ∑ j : Fin k, Real.cos (a j + m) / 2 ^ j.1 := by
simp [Finset.sum_range]
rw [h11]
specialize h_eq3 m
simpa using h_eq3
have h11 : ∑ i in Finset.range k, Real.cos (a i + n) / 2 ^ i = R0 * Real.cos (n + α) := by
have h12 : ∑ i in Finset.range k, Real.cos (a i + n) / 2 ^ i = ∑ j : Fin k, Real.cos (a j + n) / 2 ^ j.1 := by
simp [Finset.sum_range]
rw [h12]
specialize h_eq3 n
simpa using h_eq3
have h10' : R0 * Real.cos (m + α) = 0 := by
have h_eq10 : ∑ i in Finset.range k, Real.cos (a i + m) / 2 ^ i = 0 := by
linarith [h₂, h10]
linarith [h10, h_eq10]
have h11' : R0 * Real.cos (n + α) = 0 := by
have h_eq11 : ∑ i in Finset.range k, Real.cos (a i + n) / 2 ^ i = 0 := by
linarith [h₃, h11]
linarith [h11, h_eq11]
have h12 : Real.cos (m + α) = 0 := by
apply (mul_left_inj' (ne_of_gt hR0)).mp
linarith
have h13 : Real.cos (n + α) = 0 := by
apply (mul_left_inj' (ne_of_gt hR0)).mp
linarith
have h14 : ∃ m1 : ℤ, (n + α) - (m + α) = m1 * Real.pi := by
apply sub_eq_int_mul_pi_of_cos_eq_zero (m + α) (n + α) h12 h13
rcases h14 with ⟨m1, hm1⟩
use -m1
have hm4 : (m : ℝ) - (n : ℝ) = - (m1 * Real.pi) := by
have hm3 : (n + α : ℝ) - (m + α : ℝ) = (m1 : ℝ) * Real.pi := by
linarith [hm1]
nlinarith
have hm5 : (-m1 : ℤ) * Real.pi = - (m1 * Real.pi) := by
simp
rw [hm5]
linarith [hm4]
Error fixing example
In the next example, the initial proof timed out because directly applying simp to ((Real.sqrt 3 / 2 : ℂ) + (1 / 2) * Complex.I) ^ 12 resulted in excessive search complexity. Breaking down the proof by step-by-step calculating intermediate powers like $z^3$, then $z^6$, and eventually $z^{12}$ significantly reduced the computational burden on the compiler.
Sample proof of Error fixing
Proof before error fixing
import Mathlib
theorem algebra_299086 {z : ℂ} (hz : z = (Real.sqrt 3 / 2) + (1 / 2) * .I) : z ^ 2016 = 1 := by
have h1 : z = (Real.sqrt 3 / 2) + (1 / 2) * Complex.I := hz
-- Prove z^12 = 1
have h2 : z ^ 12 = 1 := by
rw [h1]
have h3 : ((Real.sqrt 3 / 2 : ℂ) + (1 / 2) * Complex.I) ^ 12 = 1 := by
simp [pow_succ, pow_zero, Complex.ext_iff, Complex.I_mul_I, mul_add, add_mul, mul_comm, mul_assoc, pow_two, pow_three, pow_succ, Real.sqrt_sq]
field_simp [Complex.ext_iff, mul_add, add_mul, pow_two, pow_three]
<;> ring_nf <;> norm_num [Real.sqrt_sq]
exact h3
calc
z ^ 2016 = (z ^ 12) ^ 168 := by ring
_ = 1 ^ 168 := by rw [h2]
_ = 1 := by norm_num
Error message
Error message:
Lean process timed out
Proof after error fixing
import Mathlib
theorem algebra_299086 {z : ℂ} (hz : z = (Real.sqrt 3 / 2) + (1 / 2) * .I) : z ^ 2016 = 1 := by
have h1 : z = (Real.sqrt 3 / 2) + (1 / 2) * Complex.I := by
exact_mod_cast hz
have h2 : z ^ 3 = Complex.I := by
rw [h1]
simp [pow_three, Complex.ext_iff, Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im, mul_add, add_mul, pow_two, mul_comm, mul_assoc]
field_simp
<;> ring_nf <;> norm_num
have h3 : z ^ 6 = -1 := by
calc
z ^ 6 = (z ^ 3) ^ 2 := by ring
_ = Complex.I ^ 2 := by rw [h2]
_ = -1 := by simp [Complex.I_sq]
have h4 : z ^ 12 = 1 := by
calc
z ^ 12 = (z ^ 6) ^ 2 := by ring
_ = (-1) ^ 2 := by rw [h3]
_ = 1 := by norm_num
calc
z ^ 2016 = (z ^ 12) ^ 168 := by
ring_nf
_ = (1) ^ 168 := by
rw [h4]
_ = 1 := by
norm_num
In case you’d wish to cite Kimina-Prover, please be happy to reference our preview paper for now. A full paper is currently in preparation and might be available soon.
@article{kimina_prover_2025,
title = {Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning},
writer = {Wang, Haiming and Unsal, Mert and Lin, Xiaohan and Baksys, Mantas and Liu, Junqi and Santos, Marco Dos and Sung, Flood and Vinyes, Marina and Ying, Zhenzhe and Zhu, Zekai and Lu, Jianqiao and Saxcé, Hugues de and Bailey, Bolton and Song, Chendong and Xiao, Chenjun and Zhang, Dehao and Zhang, Ebony and Pu, Frederick and Zhu, Han and Liu, Jiawei and Bayer, Jonas and Michel, Julien and Yu, Longhui and Dreyfus-Schmidt, Léo and Tunstall, Lewis and Pagani, Luigi and Machado, Moreira and Bourigault, Pauline and Wang, Ran and Polu, Stanislas and Barroyer, Thibaut and Li, Wen-Ding and Niu, Yazhe and Fleureau, Yann and Hu, Yangyang and Yu, Zhouliang and Wang, Zihan and Yang, Zhilin and Liu, Zhengying and Li, Jia},
yr = {2025},
url = {http://arxiv.org/abs/2504.11354},
}
[1]Team, Kimi, et al. “Kimi k1. 5: Scaling reinforcement learning with llms.” arXiv preprint arXiv:2501.12599 (2025).
[2]Qwen, et al. “Qwen2.5 Technical Report” arXiv preprint arXiv:2412.15115 (2024).
[3]Yang, An, et al. “Qwen3 technical report.” arXiv preprint arXiv:2505.09388 (2025).
[4]https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
[5]Ren, Z. Z., et al. “Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.” arXiv preprint arXiv:2504.21801 (2025).
[6]Cao, Chenrui, et al. “Reviving DSP for Advanced Theorem Proving within the Era of Reasoning Models.” arXiv preprint arXiv:2506.11487 (2025).
[7]Wang, Haiming, et al. “Kimina-prover preview: Towards large formal reasoning models with reinforcement learning.” arXiv preprint arXiv:2504.11354 (2025).
[8]https://assets.anthropic.com/m/785e231869ea8b3b/original/claude-3-7-sonnet-system-card.pdf
[9]Li, Jia, et al. “Numinamath: The biggest public dataset in ai4maths with 860k pairs of competition math problems and solutions.” Hugging Face repository 13 (2024): 9.
[10]Liu, Junqi, et al. “CombiBench: Benchmarking LLM capability for combinatorial mathematics.” arXiv preprint arXiv:2505.03171 (2025).
