From 71ba1d82ab7aeab19b240204b7556f591ea35127 Mon Sep 17 00:00:00 2001 From: Terence Tao Date: Wed, 2 Oct 2024 15:10:24 -0700 Subject: [PATCH] add percentage --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index edbf5b62..6eb5e982 100644 --- a/README.md +++ b/README.md @@ -18,7 +18,7 @@ Some automatically generated progress: - Sep 29, 2024: [13.7m implications were conjectured to be refused by a collection of 515 magmas](equational_theories/Generated/All4x4Tables), collected by enumerating all 4^(4*4) operators and reducing to a covering set. Discussed in the blueprint [here](https://teorth.github.io/equational_theories/blueprint/sect0008.html). - Oct 1, 2024: Another [~250k transitive implications](equational_theories/Generated/TrivialBruteforce) were proven by simple proof generation. Discussed in the blueprint [here](https://teorth.github.io/equational_theories/blueprint/sect0007.html). - Oct 1, 2024: [~500k transitive implications](equational_theories/Generated/EquationSearch) were proven by a custom tool that chooses hypotheses and leveraged previously found implications to search by using the implied equations as substitutions. Discussed in the blueprint [here](https://teorth.github.io/equational_theories/blueprint/sect0009.html). -- Oct 2, 2024: All but 7999 implications were [conjecturally resolved using the vampire ATP](equational_theories/Generated/Vampire). +- Oct 2, 2024: All but 7999 implications (99.958%) were [conjecturally resolved using the vampire ATP](equational_theories/Generated/Vampire). Some statistics and data files from a given point in time: - Sep 28, 2024: [A repository of unknown implications](https://github.com/amirlb/equational_theories/tree/unknown-implications), including all unknown implications, known equivalence classes, unknown implications modulo known equivalence, and only the strongest unknown implications.