Reasoning about bounded arithmetic within Lean 4

Speaker(s)

Paweł Balawender

Affiliation

MIMUW

Language of the talk

English

Date

Oct. 24, 2025, 12:15 p.m.

Room

room 5450

Title in Polish

Rozumowanie o ograniczonej arytmetyce w Lean 4

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---

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ż

---