My personal repository of formally verified mathematics.

Visual Studio Code Extension and Language Server Protocol for Coq

Cicada Language (solo version)

Cicada Language (PLCT little team)

An interactive theorem prover based on lambda-tree syntax

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

Convex optimization modeling in Lean 4

A fast, easy-to-use ring solver for agda with step-by-step solutions

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

The Slate Interactive Theorem Prover

Experiments with interactive theorem provers, LLMs and formal systems

An open source graphical proof construction assistant for the creation of Natural Deduction proofs.

A graphical web application for interactive theorem proving in Charles Peirce's alpha existential graph system.

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.

A dependent type theory logic for Isabelle

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

HLM mathematical library for the Slate interactive theorem prover

Matemáticas en Lean

Natural deduction proof assistant