Pith. sign in

REVIEW 2 major objections 5 minor 13 cited by

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

T0 review · 2 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Pairing a theorem prover with a conjecturer that generates barely provable statements doubles the fraction of LeanWorkbook provable, from 13.2% to 28.5%.

desk verdict Self-play conjecture generation beats expert iteration in formal theorem proving, but the benchmark claims need a contamination check. read the letter →

arxiv 2502.00212 v4 pith:LKZ2AJZA submitted 2025-01-31 cs.LG cs.AIcs.LO

Kefan Dong , Tengyu Ma This is my paper · ORCID
classification cs.LGcs.AIcs.LO
keywords self-playtheoremprovingconjecturinglargelanguagemodelsexpertiterationformalverificationLeanIsabellecurriculumlearning
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper claims that the standard bottleneck in training LLM theorem provers—the scarcity of correct proofs for hard statements—can be sidestepped by having the model generate its own curriculum. STP runs two roles: a prover that attempts proofs and a conjecturer that proposes new statements related to seed theorems, trained on conjectures the current prover can barely prove. Because the conjecturer is rewarded for producing statements with positive but low proof success rates, the loop continuously raises the difficulty of the generated problems and keeps providing dense training signals after expert iteration would plateau. The paper reports that 48 such iterations in Lean prove 28.5% of LeanWorkbook, double the 13.2% of expert iteration, and set whole-proof-generation best results on miniF2F-test, ProofNet-test, and PutnamBench.

What carries the argument

The engine is the conjecturer's reward: a generated statement is kept for training only if the prover's empirical pass rate lies strictly between 0 and 1/4, the proof uses the suggested lemma, and the statement survives an elegancy filter that removes conjectures whose shortest proof is too short relative to the conjecture length. A Wasserstein re-weighting then matches the selected conjectures to the distribution of still-unproved dataset statements, preventing mode collapse onto one topic. This pass-rate window creates an automated curriculum: the conjecturer is always trained on problems that are just beyond the prover's current reach.

What would settle it

Count, at each self-play round, the fraction of generated conjectures whose empirical pass rate falls in (0, 1/4] and the number of distinct seed lemmas those conjectures build on; if either number collapses to near zero within a few rounds, the mechanism has stopped generating a curriculum. A simpler decisive test is to give expert iteration the same 51.3B-token budget and the same verifier setting: if it reaches 28.5% on LeanWorkbook without any conjecturer, the conjecturer is not the cause.

Watch

Extended reading notes

Core claim

The central discovery is that the sparse-reward plateau in LLM theorem proving can be broken by making the model its own source of new problems. STP trains two roles, a conjecturer and a prover; the conjecturer receives as training data conjectures that the current prover can prove with empirical pass rate in the interval (0, 1/4], together with elegancy and diversity filters, which pushes it to emit statements that are related to, but harder than, the seed theorems. The prover is trained with standard expert iteration on the proofs of those conjectures. Run for 48 iterations in Lean with 3.6M generated conjectures, 241M generated proofs, and 51.3B generated tokens, the loop proves 28.5% of LeanWorkbook, doubling the 13.2% achieved by expert iteration, and reaches 65.0% on miniF2F-test at pass@3200.

Load-bearing premise

The whole loop depends on a pretrained model being able to keep inventing fresh, valid, learnable variants of existing theorems—problems the current prover can solve some but not most of the time—for dozens of rounds without the ideas running out or collapsing onto one topic.

Editorial extensions

If this is right

  • At the same per-iteration sample budget, the self-play loop continues to add proved statements after expert iteration has flattened, roughly doubling the fraction of LeanWorkbook proved (28.5% vs 13.2%).
  • Generated conjectures supply a denser training signal: at a checkpoint where unproved dataset statements yielded only 131 correct proofs out of 2.5M sampled, at least 47% of the generated conjectures were successfully proved, so each iteration meaningfully updates the prover.
  • The final model generalizes beyond its training statements, outperforming prior whole-proof generation methods on miniF2F-test (65.0% at pass@3200), ProofNet-test (23.9%), and PutnamBench (8/644).
  • Re-training on the generated conjectures, not just on proved dataset statements, contributes a 2–3% gain on miniF2F and ProofNet at pass@128.
  • In Isabelle, starting from a generic math-focused model, STP scales better than expert iteration or parallel sampling when compared from multiple checkpoints.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A testable extension: if the same pass-rate window and Wasserstein re-weighting are applied to natural-language math problems, the loop should sustain improvement in non-formal reasoning as well, since the difficulty signal only needs a pass/fail oracle.
  • The embedding cosine-similarity cost used for re-weighting anchors the curriculum to the current model's hidden-state geometry; replacing it with a topic-labeled distance would test whether the diversity gain is semantic or merely representational.
  • If the loop generalizes, it suggests a route toward more open-ended theorem proving without new human data: the conjecturer's job is to keep the prover inside the zone of barely provable statements, where gradient updates are most informative.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper introduces STP (Self-play Theorem Prover), a training procedure in which a conjecturer and a prover are iteratively finetuned: the conjecturer proposes new formal statements derived from seed theorems and lemmas, and the prover attempts to prove both the original unproved statements and the generated conjectures; proofs verified by Lean/Isabelle are used to train the prover, while conjectures with low-but-positive empirical pass rates, satisfying elegancy and diversity filters, are used to train the conjecturer. The authors report that with 51.3B generated tokens in Lean, STP proves 28.5% of LeanWorkbook, roughly doubling the prior expert-iteration result of 13.2%, and reports state-of-the-art whole-proof generation results on miniF2F-test (65.0% pass@3200), ProofNet-test (23.9% pass@3200), and PutnamBench (8/644). They also run an Isabelle/Llemma-7b study showing better scaling than expert iteration and parallel sampling, and an ablation showing that final retraining with generated conjectures adds 2-3% on miniF2F/ProofNet compared to retraining only on proved original statements.

Significance. The central empirical claim is significant if it holds: it suggests that self-generated conjectures can provide a sustainable source of training signal for formal theorem proving, addressing the sparse-reward plateau of expert iteration. The paper is careful in several ways: the evaluation is anchored to machine-checked proofs in Lean and Isabelle; code, model, and dataset are released; the LeanWorkbook ceiling is honestly estimated from a 20-statement manual audit; and Table 2 reports an ablation isolating the contribution of generated conjectures. The Isabelle scaling experiments from Llemma-7b provide evidence beyond a single base model. The main reservation is that the out-of-domain and SOTA claims rest on unexamined benchmark overlap with the training data, which needs to be addressed before the generalization claims can be accepted.

major comments (2)
  1. [Section 4.1, Table 1, Section 4.2] The claim in Table 1's footnote 5 that STP 'generalizes to out-of-domain theorems', and the headline SOTA numbers on miniF2F-test, ProofNet-test, and PutnamBench, are not supported because the paper reports no statement-level overlap or near-duplicate analysis between the training corpora (LeanWorkbook, miniF2F-valid, ProofNet-valid, and the base model DeepSeek-Prover-V1.5-SFT's public/proprietary SFT data) and these test sets. Since LeanWorkbook was autoformalized from natural-language math problems and the test benchmarks draw on similar competition/undergraduate sources, exact-match and semantic-equivalence duplication could inflate pass@k numbers; the STP (w/o miniF2F-valid, ProofNet-valid) row does not remove this risk because the base model was still trained on related data. I request an overlap analysis with normalization (alpha-renaming, definition unfolding) and a statement of whether any test statements were excluded from training.
  2. [Section 3.2, Appendix A.5, Table 2] The robustness of the self-play curriculum is not fully demonstrated: Appendix A.5 discloses that early experiments collapsed onto algebraic-inequality conjectures, and the Wasserstein re-weighting was added to counteract this. The paper does not ablate this re-weighting, the elegancy filter, the pass-rate window (0, 1/4], or the number K of proof samples, so it is unclear whether the improvement over expert iteration comes from the self-play loop itself or from these hand-designed diversity heuristics. Because the central claim is that conjecturing sustains improvement over many iterations (48 in Lean, 58 in Isabelle), please provide an ablation without the Wasserstein re-weighting (or with a weaker diversity regularizer) and report how quickly mode collapse occurs; this would substantially strengthen the claim.
minor comments (5)
  1. [Section 4.4] In the sentence 'See Appendx B.1', 'Appendx' is a typo for 'Appendix'.
  2. [Section 4.1] The text says 'we sample K = 32proofs per conjecture/statement'; there is a missing space before 'proofs'.
  3. [Figure 4 (Middle) caption] The caption says 'our model is not trained on miniF2F valid', but Section 4.1 states that the Lean experiments combine LeanWorkbook, miniF2F-valid, and ProofNet-valid; please clarify that this caption refers to the Isabelle experiment, or specify the exact training data for that figure.
  4. [Appendix A.6 and Figure 2] Please state explicitly which expert-iteration variant (vanilla or optimized) is used for the expert-iteration curve in Figure 2, since Appendix A.6 reports that the two variants have different sample budgets and performance.
  5. [Table 3] The PutnamBench result of 8/644 problems solved (vs. 6/644 for the prior best method) would be more convincing with an uncertainty estimate or seed variance, since the difference is only two problems on a finite benchmark.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: prover improvements are anchored to formal verifiers and external benchmarks, and the self-referential conjecture filter is an algorithmic design rather than a renamed prediction.

full rationale

The derivation chain is self-contained. STP's conjecturer reward in Section 3.2 Step 4 defines 'challenging' via the current prover's empirical pass rate P̂(c) in (0, 1/4], so selected conjectures are 'barely provable' by construction, but this is a training-signal design, not a measured prediction dressed up as a result. The headline claims — 28.5% cumulative proof rate on LeanWorkbook, 65.0% on miniF2F-test, 23.9% on ProofNet-test, and 8/644 on PutnamBench — are all checked by the Lean/Isabelle verifiers and are not equal to the selection rule; feeding selected conjectures and their verified proofs back into prover training is the intended algorithm, not a hidden fit. The Section 4.4 ablation attributes the gain to denser training signals from generated conjectures and is supported by the Isabelle scaling comparison against expert iteration and parallel sampling from the same checkpoints, as well as the final re-training ablation in Appendix B.1. No load-bearing claim rests on a self-citation: citations to the authors' prior work (Dong et al. 2024) are for hyperparameters and framing only. The absence of an overlap analysis between STP training corpora and miniF2F-test/ProofNet-test/PutnamBench is a legitimate generalization/contamination risk, but it is a correctness concern, not a circularity of the derivation. Accordingly, no specific circular reduction can be quoted, and the circularity score is 0.

Assumptions & free parameters 7 free parameters · 5 assumptions · 0 invented entities

The central claim rests on hand-chosen curriculum thresholds and training hyperparameters rather than fitted physical constants. The most consequential free choices are the (0, 1/4] pass-rate window, the elegancy quantile, and the Wasserstein matching weights, none of which are ablated. The domain assumptions are mostly standard (sound verifiers), with one fragile exception: the transfer assumption that training on self-generated conjectures improves proving on the original statements. The paper's own mode-collapse observation (Appendix A.5) shows the conjecture-generation premise is not trivially satisfied.

free parameters (7)
  • Conjecture pass-rate window (0, 1/4] = (0, 1/4]
    Conjectures are kept for conjecturer training only when the prover's empirical pass rate over K samples lies in (0, 1/4]; chosen by hand, no sensitivity analysis. Section 3.2, Step 4.
  • Elegancy filter quantile = 20% (lowest quintile removed)
    Conjectures whose minimum proof length divided by conjecture length falls in the lowest 20% are discarded; chosen by hand. Section 3.2.
  • Proof samples K per statement = 32 (STP), 64 (baselines)
    Number of independent proof attempts per item per iteration; sets the noise of the empirical pass-rate estimate and the compute budget. Section 4.1.
  • Wasserstein re-weighting cap = weight x n capped at 3 per conjecture
    Limits how much of the conjecturer training distribution a single conjecture can take; chosen by hand to stabilize training. Appendix A.5, Algorithm 4.
  • Matching weights for miniF2F-valid/ProofNet-valid = 1 for first 24 iterations, 128 afterward
    Extra weight in the Wasserstein matching for the two held-out validation splits; schedule chosen by hand, affects the conjecture distribution. Appendix A.5.
  • Length and verification-time penalties = gamma = exp(-0.001), beta = exp(-0.01)
    Reward shaping toward shorter proofs and faster verification; chosen by hand; beta applied only in Lean experiments. Sections 3.2 and 4.1.
  • Replay buffer length for the prover = 3 iterations
    Prover training uses correct proofs from the last three iterations; chosen by hand. Section 3.2.
assumptions (5)
  • domain assumption The Lean 4 and Isabelle proof checkers are sound, so every accepted proof is genuinely correct.
    Every correctness label, for both the reward signal and the benchmarks, comes from these verifiers (Section 4.1).
  • domain assumption A meaningful fraction of LeanWorkbook statements are provable translations of their natural-language originals.
    The paper's own audit (Appendix B.3) finds only 7 of 20 sampled unproved statements are provable, bounding the achievable pass rate between about 38.7% and 68.5% with 95% confidence.
  • ad hoc to paper Improvement on generated conjectures transfers to the original dataset statements and to out-of-distribution benchmarks.
    Conjectures are excluded from the LeanWorkbook metric, so the 28.5% gain must come from transfer; supported empirically (Fig. 4, Table 2) but not derived. Section 3.2.
  • domain assumption The empirical pass rate over K=32 samples orders conjecture difficulty reliably enough for curriculum selection.
    P-hat(c) is a binomial estimate with high variance at low pass rates; the paper gives no noise analysis for the (0, 1/4] selection. Section 3.2.
  • domain assumption The base model's pretraining does not leak the test sets beyond the stated miniF2F-valid/ProofNet-valid inclusion.
    The w/o-valid ablation still uses a base model pretrained on those splits (footnote 5), and overlap with PutnamBench is not analyzed. Section 4.2.

how reviews work

0 comments
Cite this review

Pith. "Pith review of STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving." pith.science (2026). https://pith.science/paper/LKZ2AJZA

@misc{pith2026250200212,
  author       = {Pith},
  title        = {Pith review of: STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LKZ2AJZA}},
  note         = {Machine review of arXiv:2502.00212}
}
read the original abstract

A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal versifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration. The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (65.0%, pass@3200), Proofnet-test (23.9%, pass@3200) and PutnamBench (8/644, pass@3200). We release our code, model, and dataset in this URL: https://github.com/kfdong/STP.

Figures

Figures reproduced from arXiv: 2502.00212 by the authors.

Figure 1
Figure 1. Self-play Theorem Prover (STP). Our model simultaneously takes on two roles — the conjecturer that [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The cumulative pass rates of STP, expert [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 4
Figure 4. Left: Cumulative pass rate on LeanWorkbook (translated into Isabelle) of STP, expert iteration, and parallel sampling, started from two checkpoints in STP training. STP achieves better scaling starting from both checkpoints. For better visualization, the x-axis starts with 50m in this figure, and we defer the full plot to [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗
Figures from the paper (1 more)
Figure 5
Figure 5. Figure 5: Left: Comparison of pass rates between STP, two implementations of expert iteration, and parallel sampling methods on LeanWorkbook. Right: Comparison of pass rates between STP and baseline methods on LeanWorkbook (Isabelle translation). The red crosses shows the points…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 13 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

    cs.AI 2026-07 accept novelty 7.0 of 10

    A distributed LLM-worker system with entropy-maximizing self-improvement generates large verified-program datasets that train open models to match Claude Opus 4.5 on verification tasks.

  2. How Your Credentials Are Leaked by LLM Agent Skills: An Empirical Study

    cs.CR 2026-04 conditional novelty 7.0 of 10

    Large-scale audit of SkillsMP agent skills finds 520 skills with 1,708 credential-leak issues, dominated by debug logging into the LLM context and hard-to-remediate forks.

  3. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  4. Anchored Self-Play for Code Repair

    cs.SE 2026-07 accept novelty 6.0 of 10

    Anchored Self-Play uses a small reference bug set and code-embedding similarity to stop generator–fixer self-play from drifting into unrealistic bugs, raising average fix rate by 7.0 points on BugSourceBench.

  5. Data-driven Machine Learning Cannot Reach Symbolic-level Logical Reasoning -- The Limit of the Scaling Law

    cs.AI 2026-06 unverdicted novelty 6.0 of 10

    Supervised deep learning cannot reach symbolic-level syllogistic reasoning due to indistinguishable training data across 24 valid types and contradictory training targets in end-to-end premise-to-conclusion mapping.

  6. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

    cs.AI 2025-07 conditional novelty 6.0 of 10

    Seed-Prover and Seed-Geometry prove 121 of 155 formalized past IMO problems, reach 99.6% on MiniF2F-test, and solve 5 of 6 IMO 2025 problems after the competition deadline.

  7. StepFun-Prover Preview: Let's Think and Verify Step by Step

    cs.AI 2025-07 conditional novelty 6.0 of 10

    A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.

  8. SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithms

    cs.LG 2025-06 conditional novelty 6.0 of 10

    Filtering self-generated math problems by a model's own solve-rate improves that model's MATH accuracy from 38% to 47% and helps out-of-distribution generalization when data is diverse.

  9. Self-Challenging Language Model Agents

    cs.AI 2025-06 conditional novelty 6.0 of 10

    A language model agent can generate its own verifiable training tasks and improve its tool-use success rate by about 2x without human-annotated data.

  10. Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning

    cs.AI 2025-07 reject novelty 5.0 of 10

    Verifier-integrated reinforcement learning with multi-turn reflection improves 7B-scale Lean 4 theorem proving by 2 to 3 points on MiniF2F at pass@128.

  11. LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving

    cs.AI 2025-06 conditional novelty 5.0 of 10

    LeanConjecturer automatically generates thousands of Lean 4 theorem statements from Mathlib files and uses them for reinforcement learning, with modest measured gains on held-out problems.

  12. Hierarchical Attention Generates Better Proofs

    cs.LG 2025-04 conditional novelty 5.0 of 10

    A hierarchical attention regularizer improves pass@64 on Lean theorem proving benchmarks by about two percentage points, while its proof-complexity reduction is computed on a small subset and is less robust.

  13. CoRT: Code-integrated Reasoning within Thinking

    cs.CL 2025-06 conditional novelty 4.0 of 10

    Inserting targeted hints into a few training examples teaches reasoning models to compute with Python instead of text, improving accuracy and cutting token use by 30 to 50 percent.

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages · cited by 13 Pith papers

  1. [1]

    All the variables are well-typed

    work page

  2. [2]

    All the functions are correctly translated into the corresponding Isabelle functions

    work page

  3. [3]

    All the symbols are correctly translated into corresponding Isabelle symbols

    work page

  4. [4]

    Here are some hints for the translation:

    Please directly output the translation without explanation. Here are some hints for the translation:

    work page

  5. [5]

    For real numbers, please use powr instead

    In Isabelle, the second operand of the operator ^ should be integer. For real numbers, please use powr instead

    work page

  6. [6]

    Please define the types of numerals

    work page

  7. [7]

    ‘Real.logb x y‘ should be translated to ‘log x y‘

    work page

  8. [8]

    ‘Real.sqrt x‘ should be translated to ‘sqrt x‘

    work page

Show all 18 references
  1. [9]

    For any variable names of form a_b, translate it to ab

    Variables with subscripts should be disallowed. For any variable names of form a_b, translate it to ab

  2. [10]

    For example, x−1 should be translated to (x powr -1)

    Please translate superscripts to the corresponding exponential form. For example, x−1 should be translated to (x powr -1)

  3. [11]

    ‘a | b‘ should be translated to ‘a dvd b‘

  4. [12]

    ‘x ≡ y [ZMOD p]‘ should be translated to ‘x mod p = y mod p‘

  5. [13]

    a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0

    ‘x ∈ zmod p‘ should represent that x is nat and x < p. ## Input: ‘‘‘lean theorem lean_workbook_50 (a b c : R) (ha : a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0) (hab : a + b + c = 3) : a^3 + b^3 + c^3 + 216 * (a * b + b * c + c * a) / (24 + a * b + b * c + c * a) ≤ 27 := by sorry ‘‘‘ ## Output: ‘‘‘...

    2023

  6. [14]

    ≤ 3 * Real.sqrt 2 := by Prove that a √ b2 + c2 + b √ c2 + a2 + c √ a2 + b2 ≤ 3 √ 2, Yes No 5 theorem lean_workbook_plus_44018 (x : R) (hx : 0 < x) (a : R ) (ha : a = x^(1/3)) : a^2 - 2 *a - (a^3 - 4) *Real.sqrt (a^3 - 7) - 3 *a^3 + 28 = 0 := by Put 3√x = a . The equation is eq...

  7. [16]

    (hz : x + y + z^3 = 1) : x = y ∧ y = z ∧ z = x := by Solve the following system of equations:   x3 + y + z = 1 x + y3 + z = 1 x + y + z3 = 1 No No 19 theorem lean_workbook_plus_51637 (A : Matrix (Fin n) (Fin n) C) (h : A * A.transpose =

  8. [17]

    Prove that A = On

    : A = 0 := by Let A ∈ Mn(C) be so that A · At = On . Prove that A = On . Here, At is the transpose of A . Yes No (not true for complex matrix) 20 theorem lean_workbook_plus_58359 (x y z : R) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : 1 ≤ x / (Real.sqrt (y * z)) * (1 / (x + 1)) +...

  9. [18]

    Yes No (when x, y, z = ϵ → 0, this term goes to 3) 25

    With 1 and √ 2 are the best constant. Yes No (when x, y, z = ϵ → 0, this term goes to 3) 25

  10. [33]

    Should be x * y) No 8 theorem lean_workbook_plus_20629 (f : R → R) (x : R) : f (f x + 1) = f x + 1 := by Prove that f (f (x) + 1) =f (x) + 1for all real x

    ≤ x2 + 2xy ≤ 1 3 q 1 2 (69 + 11 √ 33) No (there is a xy term in Lean. Should be x * y) No 8 theorem lean_workbook_plus_20629 (f : R → R) (x : R) : f (f x + 1) = f x + 1 := by Prove that f (f (x) + 1) =f (x) + 1for all real x. Yes No 9 theorem lean_workbook_37208 (n : N) (hn : ...

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.