Vision

Euled is not a fixed set of proofs: it is an algorithm. You give it a problem statement. It searches outward from the axioms (all of Mathlib) and inward from the target (the problem). It maintains a growing lemma bank of every non-trivial verified sub-lemma it discovers. When it finds a proof, it returns the result and the proof. Then it runs the Shortener cascade to tighten the proof. The cycle repeats: solve → tighten → bank → solve harder problems.

The Loop

while problems_remain:
  target = select_highest_coverage_per_cost(open_problems)
  proof = two_ended_search(target, lemma_bank)
  if proof:
    short_proof = shortener_cascade(proof)
    lemma_bank.add(short_proof.sublemmas)
    output(target, short_proof)
  else:
    open_problems.remove(target)  # or re-queue with lower priority

The forward frontier starts from Mathlib axioms and definitions. But it also incorporates all existing formalized mathematics: every theorem in Mathlib, every proof in formal-conjectures, every AlphaProof Nexus result, every FME problem. The lemma bank is the union of all verified sub-lemmas from all these sources, plus every new lemma Euled discovers.

Every output is a pair: (result, proof). The proof is a Lean 4 term that type-checks against the frozen Mathlib commit. No natural language explanations: the proof is the explanation. The site shows: statement, status, Verso-rendered proof, "run it" link (live.lean-lang.org if compatible, else lake command), and the verification checklist (Rule 2: wrapper check, axiom audit, lake build).

What Every Output Contains

• Problem statement (Lean + LaTeX)
• Verified proof (Lean term)
• Verso link (literate HTML)
• "Run it" link (live.lean-lang.org or lake command)
• Verification: wrapper check, axiom audit and lake build, each passed
• Rerun command (one-line reproduction)
• Cost: tokens, GPU-hours, $ estimate

The Shortener cascade runs on every new proof: AXLE simplify → collapse blocks → grind finish? → have2lemma + re-prove → meta-short merge. GPU neural shortener (G3) at equal compute vs ImProver-style rewriting. Idempotence test ensures CPU passes converge. The shortened proof replaces the original in the lemma bank: future searches use the tight version.

Shortener Pipeline

The same algorithm that solves Erdos problems and Putnam problems is aimed at the Millennium Prize problems formalized in Lean. Mathlib defines RiemannHypothesis: it is the expected top target by coverage-per-cost. P vs NP formalization is tracked. These are labeled as targets, not claims.

Status: not started. Once the Lean harness verifies real sub-lemmas, a launchd job on this Mac will run a continuous CPU cascade (nice 19). Frontier calls through fcc with daily cap. GPU only when idle (tag: background). It will write every 6 hours background/progress.json with: bridge distance to target, non-trivial verified sub-lemmas on best path, bank size and reuse, open subgoals on best path, CPU-h, GPU-h, fcc calls, tokens.

Notification Policy

• Notify (ntfy.sh + email) ONLY after: Rule 2 in full against Mathlib's RiemannHypothesis + clean rebuild on fresh machine + independent fresh-agent re-check
• Weekly progress push (no notification, just log)
• Failed/suspicious solves → background/false_alarms.md (never notify)

Optimize the Optimization

• Weekly Optuna: closer order, timeouts, bank top-k, middle-point count, frontier-call threshold
• Objective: non-trivial sub-lemmas on target path per token (held-out slice)
• Monthly: coverage-per-cost engine tunes the weekly search itself
• Stop when expected gain from more tuning < compute cost of tuning
• Keep change only if it beats previous on held-out slice; log before/after in DECISIONS.md

This work builds on:

• DeepMind: AlphaProof, AlphaProof Nexus, formal-conjectures
• Epoch AI: LeanOpenProblems (FME), forecasting
• Mathlib: The mathematics library
• UW Math AI: TheoremGraph, LeanGraph, LeanExplore
• Axiom: AXLE (verify_proof, simplify_theorems, have2lemma, disprove)
• Numina: Goedel-Prover models
• Goedel-LM: Goedel-Prover-V2-8B
• Questboy23: ai-math-forecast (dated Erdős forecast)