Aiming to have a personal well-founded math library written in lean. Hope it works...
-
Updated
Jan 7, 2023
Aiming to have a personal well-founded math library written in lean. Hope it works...
Homeworks for 'formal languages and grammars' discipline
Coq Formalisation of "A Fine-Grained Evaluation Strategy for Delimited-Control Operators shift0/dollar"
Categorical Semantics of Intuitionistic Multiplicative Linear Logic written in Isabelle/HOL
Repository hosting resources for the 2024 workshop "Computer-Verified Proofs: 48 Hours in Rome" organised by @oliver-butterley, @RafaelGreenblatt and @marcolenci.
The stages that Blue Husky Studios goes throguh when creating a product
This repository will eventually contain the code I wrote when formalising the Dedekind-Kummer Theorem
An unusual construction of the real numbers using Isabelle/HOL
Repository hosting resources for the 2024 workshop "Lean for the Curious Mathematician".
All MMT archives of formalizations needed by the UFrameIT prototype in the FrameIT project.
The back end of a tool for checking formalization exercises.
Modern forms finally made easy.
We prove the equivalence between three induction principles for the untyped lambda calculus.
Repository hosting resources for the 2024 course in Formal Mathematics at @ImperialCollegeLondon taught by Kevin Buzzard (@kbuzzard).
The front end of a tool for checking formalization exercises.
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
Collaborative repo for Big Proof Programme at the Isaac Newton Institute, Jun 26 to Aug 4, 2017
Trabajo de Fin de Grado de Matemáticas, en la Universidad Complutense de Madrid. Presentado en septiembre de 2023.
Formalization of Robin Milner's bigraphs in Isabelle/HOL
Add a description, image, and links to the formalization topic page so that developers can more easily learn about it.
To associate your repository with the formalization topic, visit your repo's landing page and select "manage topics."