Formal verification of GT-SMDN framework in Lean 4. 53 theorems formalised, 28 complete proofs. Companion to 'Protecting Critical Infrastructure' book.

Formalization projects for the Foundation of Software course at EPFL

This project aims to formalize some concepts of Automata Theory and Parsing into Lean4 Theorem Prover. This was a course project for the course 'Proofs and Programs' offered by Prof Siddhartha Gadgil at IISc, Spring 2025.

DAO (Demostración Asistida por Ordenador) con Lean

A formalization of exercise 3.16 of Grifone's "Algèbre Linéaire" in the Lean Theorem prover

Writing some propositions and giving some proofs in Lean

Lean4 is a purely functional programming language based on the calculus of constructions with inductive types. Formal verification of claims are expressed in precise mathematical terms.

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.

Materijali za radionicu interaktivnog dokazivanje teorema @ IS Petnica

A Lean 4 eDSL for writing declarative, correct-by-construction packing lists for user defined expeditions (e.g. walking the Camino, hiking the CDT, dressing for a wedding)

Lean Subtypes that have Super powers

A (successful !) attempt at computing the Gaussian integral in Lean

Exercises from Theorem Proving In Lean

monoidal categories in the Lean theorem prover

A newbie's reference solutions to Lean tutorials

Proof of soundness of the Unit-B refinement calculus

A repository for studying and implementing Lean theorems, focusing on mathematical and philosophical concepts.

Step-by-step small or medium-sized projects in Lean