Reasoning about bounded arithmetic within Lean 4

Prelegent(ci)

Paweł Balawender

Afiliacja

MIMUW

Język referatu

angielski

Termin

24 października 2025 12:15

Pokój

p. 5450

Tytuł w języku polskim

Rozumowanie o ograniczonej arytmetyce w Lean 4

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Teorie nowoczesnych asystentów dowodowych (np. Rocq, Lean, Mizar) mają
bardzo dużą siłę wyrazu. Zazwyczaj jest to cecha pożądana, bo chcemy by
te narzędzia były w stanie weryfikować dowody trudnych twierdzeń. Czasem
jednak chcemy rozumować w słabszej teorii. Przykładem może być
rozumowanie bez aksjomatu wyboru, jednak rozważymy systemy dużo słabsze
- arytmetyki ograniczone. Podczas referatu zaprezentuję dwa sposoby na
użycie Leana lub Rocqa do przeprowadzania dowodów wewnątrz arytmetyk
ograniczonych, tak by użytkownik nie mógł „oszukiwać” poprzez
zastosowanie faktu prawdziwego w meta-teorii a w  badanej teorii już

---

The theories of modern proof assistants (e.g. Rocq, Lean, Mizar) are highly expressive. This is usually a desirable feature, since we want these tools to be capable of verifying proofs of complex theorems. However, sometimes we wish to reason within a weaker theory. An example might be reasoning without the axiom of choice. Still, we want to focus on even weaker systems, bounded arithmetics.

In this talk, I will present two approaches to using Lean or Rocq for conducting proofs within bounded arithmetics, in such a way that the user cannot `cheat' by applying a fact that holds in the meta-theory but not in the theory being studied.

---