Libraries
Statements a person can read
A formalization that only another formalizer can parse has done half the work. Each deposit should carry the informal statement, the system, the axioms actually used, and a pointer to the checked source.
Research
Formalization as a
mathematical activity.
The prospectus covers more than the last line of a proof. Formalization includes the definitions, the library, the choice of foundations, and the use of machines that suggest the next step.
Research themes
- 01
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.
- 02
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.
- 03
Artificial 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.
- 04
Mathematical 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.
The principle
When the model speaks,
the kernel signs.
Generated text is a proposal. Acceptance belongs to a checker whose rules are public.
Questions to work on
Beyond the last line.
Definitions, foundations, and the meaning
of a checked statement.
Assistants
Several kernels, one conversation
Lean, Rocq, Isabelle, and Agda do not formalize the same way. The institute would not pick a house system in order to look decisive. Translation, and honesty about what does not translate, is part of the subject.
Models
Proposal, then refusal
Autoformalization and lemma search are already changing the pace of formal work. The research stance here is narrow on purpose: generated text is a proposal. Acceptance belongs to a checker whose rules are public.
Foundations
What the certificate does not say
A machine-checked proof certifies a statement in a logic. It does not, by itself, certify that the statement is the theorem mathematicians meant. That gap — between informal intent and formal claim — is a research topic, not an embarrassment.