A high-fidelity formal modeling and verification framework for complex system architectures, powered by Lean 4.

Provide a verified, machine-checked constructive reduction of the Cook-Levin theorem from Turing machines to SAT formulas using Lean 4.

Prove the non-existence of perfect cuboids using formal methods and algebraic structures verified in Lean 4 with detailed mathematical analysis.

A Proof-oriented Programming Language

The Beal Symmetry Collision: A Machine-Certified Solution via p-adic Valuations

Formal Proof of the Non-Existence of Perfect Cuboids via Mordell-Weil Rank Exhaustion and Minimal Polynomial Irreducibility of the Perfect Cuboid Surface.

A verified constructive reduction of the Cook-Levin Theorem in Lean 4.

A Formally Verified Structural Parity Proof of the Collatz Conjecture.

A Formal Proof of the Non-Existence of Odd Perfect Numbers for Euler Primes p ≥ 5 via Structural Divisibility Constraints.

My personal repository of formally verified mathematics.

Doodles in Lean.

A formal verification of an abstract SAT solving transition system.

HOL Light Library for Modal Systems

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

A Lean 4 formalization of discrete causal posets and convex-cone models for AQEI constraints. Features 130+ machine-checked theorems covering chain-complex homology proxies, $Z_1$ cycle space stability, and bidirectional equivalence of 1-cycle proxies.

HOL-Light Library for Modal Systems

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]

An experimental workspace for my master's thesis in interactive theorem proving

An interactive theorem prover based on lambda-tree syntax

Lean 4 workshop: tutorials, proofs, and learning resources