Florent Schaffhauser's Projects
GitHub repository for the Proseminar on Computer-assisted mathematics held at the University of Heidelberg in Summer Semester 2023.
GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summer Semester of 2024.
The Leek group guide to data sharing
Domain-Specific Languages of Mathematics
Repository for the September 2023 Hausdorff School on Lean
Some material for Lean 4 lectures at IISc
ๆฐๅญฆ็ณปใฎใใใฎLeanๅๅผทไผ
A tool to auto-generate and render slides from Markdown comments in the Lean editor.
Resources to teach Linear Algebra using Lean4 and Sagemath
Lean package template (without a Mathlib dependency)
Repository for the conference LFTCM2024
Coq/Rocq practice session @ Lean For The Curious Mathematicians 2024
Personal webpage
The user home repository for the Mathematics in Lean tutorial.
Lean package template (with a Mathlib dependency)
Create book from markdown files. Like Gitbook but implemented in Rust
Tool to generate markdown files from lean files. This is heavily inspired by lean2md.
An introduction to programming language theory in Agda
Theorems for Real Closed Fields
Formalisation in Lean 4 of basic results in Real Algebraic Geometry
Materials for my lecture at the 2023 International School on Interactions of Proof Assistants and Mathematics in Regensburg
Summing squares in Lean
LaTeX template repository
Theorem Proving in Lean 4