In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources: a natural language ...

Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL...

Computational paths treat propositional equality as explicit paths built from labelled deduction steps and rewrite rules. This view originates in work by de Queiroz and collaborators and yields a weak...

The readings shared in Bluesky on 24 November 2025 are: An introduction to formal real analysis (Lecture 21: Functions and derivatives). ~ Alex Kontorovich. #ITP #LeanProver #Math A perspective on in

Descriptive set theorists study the niche mathematics of infinity. Now, they’ve shown that their problems can be rewritten in the concrete language of algorithms.

YouTube video by Icelandic Centre of Excellence in Theoretical CS

YouTube video by Icelandic Centre of Excellence in Theoretical CS

Into an interactive theorem provers (ITPs), one can write mathematical definitions, theorems and proofs, and the correctness of those results is automatically checked. This perspective goes over the ...

**Abstract:** This paper introduces a novel framework for automated formalization and verification of concurrent reactive systems, leveraging the expressive power of Lean 4’s dependent type theory and the Alloy Analyzer's powerful constraint solving capabilities. We present an integrated system that automatically translates Alloy specifications of concurrent systems (e.g., protocols, distributed algorithms) into Lean 4 code, enabling comprehensive formal verification utilizing Lean’s theorem prover and property checker.

YouTube video by Alex Kontorovich

During the last decade, the domain of Qualitative Spatial Reasoning, has known a renewal of interest for mereogeometry, a theory that has been initiated by Tarski. Mereogeometry relies on mereology, t...

We set out a general methodology for producing tableau systems for propositional logics via a tableau metatheory that provides general and formal notions for different tableau systems that vary by sem...

Qualitative spatial models based on Goodman-style mereology and pseudo-topology often pose problems for advanced geometric reasoning, as they lack true Euclidean geometry and fully developed topologic...

The readings shared in Bluesky on 23 November 2025 are: DeepMind’s latest: An AI for handling mathematical proofs. ~ Jacek Krywko. #AI #Math #LLMs #ITP #LeanProver #AlphaProof Verified certification

The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why. We describe a formal proof that the adele ring of a number field is locally compact implemented in the Lean 4 theorem prover. Our work includes the formalisations of new types, including the completion of a number field at an infinite place, the infinite adele ring and the finite $S$-adele ring, as well as formal proofs that completions of a number field are locally compact and that their rings of integers at finite places are compact.