Fix, nicht nur Resample: Bounded Compiler-gesteuerte Reparatur in Lean 4

arXiv:2610.26942v1 Automatische Theorem-Prover verlassen sich oft auf Sampling von Language Models, aber Proof Assistants wie Lean lehnen jeden fehlgeschlagenen Schritt mit einer präzisen Fehlermeldung ab - Informationen, die reines Sampling verwirft. Um dies zu überwinden, führen wir einen bounded Online-Schritt-Level ein