aⁿ + bⁿ ≠ cⁿ, n > 2
Fermats letzter Satz, maschinell geprüft
Für n größer als zwei gibt es keine positiven ganzen a, b, c mit aⁿ + bⁿ = cⁿ. Der Satz war bereits bewiesen; Claude formalisierte ihn.
Fachkommentar↗
Formal verification
Inspect the formal statement, imported axioms, admitted lemmas, checker version and correspondence with the informal theorem. A successful compiler exit alone does not prove that the intended question was formalized.
Erklärte Dossiers
Forschungsnotizen
h1: A Taste of the Bitter Lesson in Automated Theorem Proving
Formal verification · preprint
While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
Formal verification · preprint
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Maestro: Agentic Formal Proof Development by Coordination
Formal verification · preprint
Lean is increasingly used to verify mathematical proofs and software produced by LLM agents, but writing formal proofs remains hard. Existing prover systems take a
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Attention-Graph Curvature for the Verification of Mathematical Reasoning
Formal verification · preprint
Language models have recently solved open Erdős problems and achieved gold-medal level performance on International Mathematical Olympiad problems. But their solutions, written in natural language,
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
Formal verification · preprint
We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
Formal verification · preprint
Program verification establishes software correctness through machine-checkable proofs constructed in theorem provers. It's a guarantee especially valuable for code generated by large language models (LLMs),
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
Formal verification · preprint
In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Sharing AI progress in mathematics
Formal verification · provider_announcement
OpenAI publishes new results on open problems in mathematics from an internal frontier model and shares Lean proof formalizations and research details on GitHub.
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Preserving Mathematical Reasoning in Compressed Diffusion Language Models via Trajectory-Aware Low-Rank Approximation
Formal verification · preprint
Diffusion language model (dLLM) compression faces a known challenge because calibration is typically performed on clean, fully visible activations, whereas inference traverses partially masked intermediate
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗When Does Structured Knowledge Help Neural Theorem Proving?
Formal verification · preprint
Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving
Formal verification · preprint
Neural theorem provers must both propose tactics and decide which valid successor states to explore. We study whether one-step Lean transitions provide a self-supervised signal
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗Direct Optimization of Generators for Search in Automated Theorem Proving
Formal verification · preprint
Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt
Automatisch gesichtet · hier nicht fachlich begutachtetForschungsnotiz lesen ↗