Formalized mathematics
Definitions, constructions, and theorems written so a proof kernel can check them — libraries that travel, not notes that only a specialist can reconstruct.
ExploreFounding prospectus · Bologna
Artificial logic,
made checkable.
A European institute for formalized mathematics, computer-verified proofs, and the logics a machine can follow.
Meaning guides. Syntax decides.
Four connected fields
Computer-assisted proof
Proof assistants as instruments of mathematical work: Lean, Rocq, Isabelle, Agda, and the translations between them. The checker, not the interface, is the authority.
ExploreArtificial logic
Models that propose lemmas, translations, and proof sketches. A proposal is not a proof. Artificial logic earns its name when a machine can follow the rule, and a kernel can refuse it.
ExploreMathematical logic
The ground under the tools: type theory, proof theory, computability, and the limits of what a formal system can certify. Foundations treated as a living subject, not a preface.
ExploreThe distinction
Two logics.
One written down.
Late medieval and early modern writers separated logica naturalis — the inborn capacity to argue — from logica artificialis, the formal art: rules made explicit, taught, and inspected.
The second name is the one we take. A proof assistant, a verified library, an AI that proposes a lemma and a kernel that accepts or refuses it: these are artificial logic in the old sense, carried into mathematics that can be replayed.
Read the longer noteA first shape of work
From a statement
to a shared practice.
A proposed programme for the institute.
These activities are not yet scheduled.
- 01
A shared library
Formalizations deposited with statements a mathematician can read, and sources a checker can replay. Not bound to a single assistant.
- 02
Working seminars
Short, public sessions on a theorem in the process of being formalized — including the places the formalization resists the informal proof.
- 03
Residencies
Time in Bologna for mathematicians who want to formalize a result they already understand, with people who know the assistants.
- 04
A note series
Brief, citable notes: what was formalized, in which system, under which axioms, and what was left informal on purpose.
A place for the conversation
Bologna, Europe.
The University of Bologna is the Alma Mater Studiorum. The institute would sit in that city without pretending to be the university, and would work in the open with groups already formalizing mathematics across Europe.
Write to the prospectus