A verification toolchain for Rust programs

A pure-Rust implementation of group operations on Ristretto and Curve25519

Verifying curve25519-dalek using Lean

Home to the Signal Protocol as well as other cryptographic primitives which make Signal possible.

Technical report of Kimina-Prover Preview.

A formalized proof of Carleson's theorem in Lean

GitHub Action to compile LaTeX documents

Compares two latex files and marks up significant differences between them. Releases on www.ctan.org and mirrors

List of the output of #help command of mathlib4, including list of all tactics, commands...etc

GitHub action for standard CI in Lean projects

GitHub action for standard CI in Lean projects

A GitHub action to create a pull request for changes to your repository in the actions workspace

The action attempts to update Lean and Mathlib. If an update is available then the updated version is tested. This allows for automatic committing of the updated project, opening PRs or opening iss…

VS Code extension for the Lean 4 programming language and theorem prover

Introduction to dynamical systems

The math library of Lean 4

Github action to verify file changes that occur during the workflow execution.

Project for "Machine-Checked Mathematics" at the Lorentz Center

Birkhoff's ergodic theorem in Lean

Render images occurring by itself in a paragraph as `<figure>< img ...></figure>`, similar to pandoc's implicit_figures

Website for the formalisation of mathematics and Lean event in Rome

Personal webpage