Issues

• AP Lite solution: substInv_X_sub_X_sq_eq_catalan

  leanprover/lean-eval-submissions#1987 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: oppenheim_inequality

  leanprover/lean-eval-submissions#1986 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: brauer_character_in_cyclotomic

  leanprover/lean-eval-submissions#1985 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: posSemidef_map_exp

  leanprover/lean-eval-submissions#1984 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: sturm_separation

  leanprover/lean-eval-submissions#1983 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: mulCayley_connected_iff_closure_eq_top

  leanprover/lean-eval-submissions#1982 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: cubic_decay_asymptotic

  leanprover/lean-eval-submissions#1981 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: bvp_comparison

  leanprover/lean-eval-submissions#1980 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: dirichlet_eigenvalues_eq_nat_sq

  leanprover/lean-eval-submissions#1979 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solution: finite_graph_ramsey_theorem

  leanprover/lean-eval-submissions#1978 · Filter by author axiom-agents-internal opened on Oct 5, 2026

• AP Lite solutions for nine legacy lean-eval problems

  leanprover/lean-eval-submissions#1977 · Filter by author axiom-agents-internal opened on Oct 5, 2026
  1

• [submission] sphere_theorem_topological — max gp (GPT-6) — @ma4ypic4y @haskiindahouse

  submission
  leanprover/lean-eval-submissions#1975 · Filter by author ma4ypic4y opened on Oct 5, 2026

• TauCeti cache intermittently aborts submission evaluation

  leanprover/lean-eval-submissions#1894 · Filter by author Vilin97 opened on Oct 1, 2026

• OAuth callback returns 503 state_unavailable after successful GitHub authorization (reproducible, 2026-09-18 ~04:05–04:25 UTC)

  leanprover/lean-eval-submissions#1739 · Filter by author mlgraham opened on Sep 18, 2026
  1

• Kernel-heavy submissions: 360-min job with single-threaded nanoda replay caps decide +kernel work at ~10 CPU-h — is a larger budget or parallel replay possible?

  leanprover/lean-eval-submissions#1697 · Filter by author mlgraham opened on Sep 10, 2026
  1

• Reduce single-problem evaluation latency without weakening the sandbox

  leanprover/lean-eval-submissions#1616 · Filter by author kim-em opened on Sep 2, 2026

• Operate the four-week server-intake overlap and retire issue intake

  leanprover/lean-eval-submissions#1610 · Filter by author kim-em opened on Sep 2, 2026

• Migrate recoverable private archives to per-submission key envelopes

  leanprover/lean-eval-submissions#1609 · Filter by author kim-em opened on Sep 2, 2026

• Complete final-corpus replay with the official Lean kernel and nanoda

  leanprover/lean-eval-submissions#1608 · Filter by author kim-em opened on Sep 2, 2026

• Finalize the issue-cutoff corpus and append-only historical inventory delta

  leanprover/lean-eval-submissions#1607 · Filter by author kim-em opened on Sep 2, 2026

• [submission] Abel–Ruffini — MathGraph + GPT-5.6 Sol

  leanprover/lean-eval-submissions#1449 · Filter by author heathsanchez opened on Aug 27, 2026

• evaluate OOMs on 16 GB hosted runners for memory-heavy submissions (exit 143, misleading failure comment)

  leanprover/lean-eval-submissions#1078 · Filter by author Vilin97 opened on Aug 16, 2026
  1

• [submission] MerLean finished proofs

  leanprover/lean-eval-submissions#585 · Filter by author CollinYuanjieRen opened on Jul 6, 2026