From 6b407e43fde46b266c1042ede20bc01ff2f06ec8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 4 Nov 2023 14:35:01 +0100 Subject: [PATCH] mathlib is now ported to Lean 4 --- README.md | 6 ------ 1 file changed, 6 deletions(-) diff --git a/README.md b/README.md index 2228ccca88..565c1730d7 100644 --- a/README.md +++ b/README.md @@ -24,12 +24,6 @@ constant `c > 0`. This is an amazing improvement over previous bounds, which wer The formal system which we are using as a target system is Lean's dependent type theory. Lean is a project being developed at AWS and Microsoft Research by Leonardo de Moura and his team. -At this stage, mathlib4 contains all the background material that we need. However, not all -quality-of-life improvements that we know from Lean 3 have made it to Lean 4 (yet) and Lean 4 -suffers from its own problems that currently make it unsuitable for new formalisation of -research-level mathematics. As a consequence, we are sticking to Lean 3 until the project is -complete. Then we will port it to Lean 4 in order to upstream our basic results. - ## Content of this project This project currently contains about 3k lines of Lean code about the discrete (difference)