A formal verification of Linear PCP SNARKs.

Riemann Hypothesis in Lean

A formalization of graded rings in Lean, corresponding to a CICM 2022 submission

Formalising non-commutative graph theory in Lean

Materijali za radionicu interaktivnog dokazivanje teorema @ IS Petnica

A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover.

This repository contains a collection of mathematical exercises in Lean, covering topics like geometric series, binomial coefficients, and recursive functions. Ideal for learning formal proofs with Lean's theorem prover.

A semester project for an introduction to interactive theorem proving using LEAN4 language and Mathlib library

Formalization of Euler's polyhedron formula (V - E + F = 2) in Lean 4

This repository holds exercises and solutions for the Lean for the Curious Mathematician 2023 (LftCM2023) workshop. Focused on formal mathematics with Lean 4, it provides a hands-on learning experience based on the "Mathematics in Lean" book. Updated in October 2024, it includes solutions and resources for exploring proofs and formal logic.

Attempt to formalize salsa20 in lean

Reals defined using Quasi-Morphisms formalized in Lean

Lean 4 formalization of Unlimited Register Machines for CSLib

Operator-theoretic proof of the Twin Prime Conjecture via Sobolev spaces (Lean 4)