Targeted Formal Conjectures audit report

Targeted Formal Conjectures audit

• Result: failure
• Repository: DomTheDeveloper/formal-conjectures
• Commit: 1950557db4addd18fa221195eb30a2ecd76bfa86
• Module: FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentToReduced
• Source: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentToReduced.lean
• Run: https://github.com/DomTheDeveloper/ProofPlaygrond/actions/runs/30022326305

Compiler excerpt

✖ [7884/7901] Building FormalConjectures.Arxiv.«2508.10245».Geode5 (156ms)
trace: .> LEAN_PATH=/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/bin/lean /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/FormalConjectures/Arxiv/2508.10245/Geode5.lean -o /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5.olean -i /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5.ilean -c /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5.c --setup /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5.setup.json --json
error: FormalConjectures/Arxiv/2508.10245/Geode5.lean:17:0: unknown module prefix 'FormalConjecturesUtil'

No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean
/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean
/home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean
error: Lean exited with code 1
ℹ [7892/7901] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentAlgebra (5.7s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean:115:0: 'Arxiv.«2508.10245».Geode5Proof.moment_division_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean:116:0: 'Arxiv.«2508.10245».Geode5Proof.momentQuotient_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentAlgebra.lean:117:0: 'Arxiv.«2508.10245».Geode5Proof.recurrenceDiagonal_product' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7893/7901] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Integral (11s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/Integral.lean:91:0: 'Arxiv.«2508.10245».Geode5Proof.integral01_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7897/7901] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.Recurrence (7.8s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/Recurrence.lean:130:0: 'Arxiv.«2508.10245».Geode5Proof.qMoment_recurrence_raw' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [7899/7901] Built FormalConjectures.Arxiv.«2508.10245».Geode5Proof.RecurrenceStep (16s)
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceStep.lean:168:0: 'Arxiv.«2508.10245».Geode5Proof.integral01_qSparsePolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/RecurrenceStep.lean:169:0: 'Arxiv.«2508.10245».Geode5Proof.integral01_qMomentQuotient' depends on axioms: [propext, Classical.choice, Quot.sound]
✖ [7900/7901] Building FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentFormula (4.4s)
trace: .> LEAN_PATH=/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Cli/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/batteries/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/Qq/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/aesop/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/importGraph/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/plausible/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/packages/mathlib/.lake/build/lib/lean:/home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.27.0/bin/lean /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean -o /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.olean -i /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/lib/lean/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.ilean -c /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.c --setup /home/runner/work/ProofPlaygrond/ProofPlaygrond/target/.lake/build/ir/FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.setup.json --json
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:54:18: unsolved goals
case add.h_add
A m : ℕ
p q : Polynomial ℚ
hp : ((Polynomial.X + 1) ^ A * p.comp (Polynomial.X + 1)).coeff m = p.sum fun j a ↦ a * ↑((A + j).choose m)
hq : ((Polynomial.X + 1) ^ A * q.comp (Polynomial.X + 1)).coeff m = q.sum fun j a ↦ a * ↑((A + j).choose m)
⊢ ∀ (a : ℕ) (b₁ b₂ : ℚ), (b₁ + b₂) * ↑((A + a).choose m) = b₁ * ↑((A + a).choose m) + b₂ * ↑((A + a).choose m)
error: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:61:23: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  Polynomial.C ?m.120 * Polynomial.C ?m.121
in the target expression
  ((Polynomial.X + 1) ^ A * Polynomial.C a * (Polynomial.X + 1) ^ n).coeff m =
    ((Polynomial.monomial n) a).sum fun j a ↦ a * ↑((A + j).choose m)

case monomial
A m n : ℕ
a : ℚ
 Quot.sound]
info: FormalConjectures/Arxiv/2508.10245/Geode5Proof/MomentFormula.lean:76:0: 'Arxiv.«2508.10245».Geode5Proof.momentCoefficient_eq_extractionSum' depends on axioms: [propext,
 sorryAx,
 Classical.choice,
 Quot.sound]
error: Lean exited with code 1
Some required targets logged failures:
- FormalConjectures.Arxiv.«2508.10245».Geode5
- FormalConjectures.Arxiv.«2508.10245».Geode5Proof.MomentFormula
error: build failed

Reproduce the failed build from the linked Actions run, then inspect FormalConjectures/Arxiv/2508.10245/Geode5.lean and Geode5Proof/MomentFormula.lean alongside the reported errors. The work is done when the missing FormalConjecturesUtil module and the listed unsolved goals no longer prevent the project build from succeeding.