# Automatyczne dowodzenie twierdzeń (Lean)

EN: **Automated and formal theorem proving (Lean)** · id `theoremproving`

Path: [AI Atlas](https://aiatlasgraph.com/llms.txt) › [Fundamenty i rozumowanie](https://aiatlasgraph.com/t/foundations.md) › [Logika i reprezentacja wiedzy](https://aiatlasgraph.com/t/logic.md) › Automatyczne dowodzenie twierdzeń (Lean)

## Description

- PL: Modele generują formalne dowody sprawdzane przez jądro systemu takiego jak Lean. Weryfikacja potwierdza poprawność zaakceptowanego dowodu względem sformalizowanego twierdzenia, zadeklarowanych aksjomatów i zaufanego jądra; poprawność autoformalizacji pozostaje osobnym zagadnieniem.
- EN: Models generate formal proofs checked by the kernel of a system such as Lean. Verification establishes that an accepted proof is correct relative to the formalized statement, declared axioms, and trusted kernel; the faithfulness of autoformalization remains a separate issue.

## In one sentence

- PL: To szukanie i sprawdzanie matematycznych dowodów zapisanych w ścisłym języku.
- EN: This finds and checks mathematical proofs written in a precise formal language.

## Problem it solves

- PL: Przekonujące wyjaśnienie może zawierać ukryty błąd; potrzebujesz dowodu, którego każdy krok da się sprawdzić.
- EN: A convincing explanation may hide an error; you need a proof whose every step can be checked.

## What it does

- PL: Sprawdza kroki dowodu względem zapisanych reguł i założeń; poprawne przełożenie pierwotnego pytania na ten zapis wymaga osobnej kontroli.
- EN: It checks proof steps against recorded rules and assumptions; translating the original question correctly into that language requires separate checking.

## Everyday example

- PL: Asystent proponuje dowód wzoru na sumę kolejnych liczb, a program sprawdza, czy kroki wynikają z przyjętych założeń.
- EN: An assistant proposes a proof for a formula summing consecutive numbers, and software checks whether the steps follow from the assumptions.

## This concerns you if you…

- PL: potrzebujesz sprawdzić rozumowanie krok po kroku
- PL: pracujesz z twierdzeniami wymagającymi ścisłego dowodu
- EN: need reasoning checked step by step
- EN: work with statements requiring a rigorous proof

## Keywords

Lean 4 · mathlib · miniF2F · autoformalization · proof assistants · proof kernels

## How it works

- PL: Generator lub taktyki budują formalny term dowodu, przeszukując dopuszczalne kroki. Niewielkie jądro sprawdza ten term względem systemu typów, zadeklarowanych aksjomatów i dokładnie zapisanego twierdzenia.
- EN: A generator or tactics construct a formal proof term by searching permitted steps. A small kernel checks it against the type system, declared axioms and the precisely stated theorem.

## Limits

- PL: Weryfikacja nie potwierdza poprawności przekładu zadania z języka naturalnego. Zaufanie obejmuje jądro i aksjomaty; poszukiwanie dowodu może być kosztowne lub nie zakończyć się sukcesem.
- EN: Verification does not establish faithful translation from natural language. Trust includes the kernel and axioms; proof search can be costly or unsuccessful.

## Key terms

- PL: **term dowodu**: Formalny obiekt reprezentujący uzasadnienie sprawdzane przez system typów.
- PL: **jądro**: Mały komponent odpowiedzialny za ostateczne sprawdzanie poprawności formalnej dowodu.
- EN: **proof term**: A formal object representing a justification checked by the type system.
- EN: **kernel**: A small component responsible for final formal proof checking.

## Know first

- [Logika zdań i logika pierwszego rzędu (Propositional and first-order logic)](https://aiatlasgraph.com/t/fol.md)

## Examples

- PL: Lean 4 · autoformalizacja · miniF2F · zadania olimpijskie
- EN: Lean 4 · autoformalisation · miniF2F · olympiad problems

## Related topics

Untyped, symmetric "see also" links.

- [Automatyzacja badań naukowych (AI-driven scientific discovery and research automation)](https://aiatlasgraph.com/t/discovery.md)
- [RL z weryfikowalnymi nagrodami (RLVR) (Reinforcement learning with verifiable rewards)](https://aiatlasgraph.com/t/rlvr.md)
- [Solwery SAT i SMT (SAT and SMT solvers)](https://aiatlasgraph.com/t/satsmt.md)
- [Sprawdzanie końcowego wyniku (Outcome verification)](https://aiatlasgraph.com/t/outcomeverify.md)

## Sources

- [Olympiad-level formal mathematical reasoning with reinforcement learning (AlphaProof)](<https://www.nature.com/articles/s41586-025-09833-y>) `alphaproof2025` · by Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth i in. (Google DeepMind)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](<https://arxiv.org/abs/2507.23726>) `seedprover2025` · by Luoxin Chen, Jinming Gu, Liankai Huang i 34 współautorów
- [Lean Reference Manual — the kernel and proof-term checking](<https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/#the-kernel>) `lean-reference-kernel` · by Lean Project

---

AI Atlas revision 122 (2026-10-30) · HTML: https://aiatlasgraph.com/t/theoremproving · index: https://aiatlasgraph.com/llms.txt · everything: https://aiatlasgraph.com/llms-full.txt · updated 2026-10-30