From 15d5417f8a3d141a7dc84303c8da07e564af005c Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Wed, 2 Oct 2024 18:01:35 -0400 Subject: [PATCH 1/3] fix dashboard url (#208) --- home_page/_layouts/default.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/home_page/_layouts/default.html b/home_page/_layouts/default.html index 3ff9adb4..40308185 100644 --- a/home_page/_layouts/default.html +++ b/home_page/_layouts/default.html @@ -30,7 +30,7 @@

{{ page.description | default: site.description | de Blueprint (web) Blueprint (pdf) Documentation - Dashboard + Dashboard {% if site.github.is_project_page %} GitHub {% endif %} From 4981101073cd851ec669dab6e88a11bce54ad42c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9s=20Goens?= Date: Thu, 3 Oct 2024 00:03:46 +0200 Subject: [PATCH 2/3] add three new implications to subgraph that were found with lean-egg (#207) * add three new implications to subgraph that were found with lean-egg * Type* and remove minor cleanup --- equational_theories/Subgraph.lean | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/equational_theories/Subgraph.lean b/equational_theories/Subgraph.lean index 0ec5dbb5..f571e5e1 100644 --- a/equational_theories/Subgraph.lean +++ b/equational_theories/Subgraph.lean @@ -352,6 +352,29 @@ theorem Equation4582_implies_Equation4564 (G: Type*) [Magma G] (h: Equation4582 theorem Equation4582_implies_Equation4579 (G: Type*) [Magma G] (h: Equation4582 G) : Equation4579 G := fun _ _ _ _ _ ↦ h _ _ _ _ _ _ +/- Obtained with lean-egg -/ +@[equational_result] +theorem Equation14_implies_Equation23 (G: Type*) [Magma G] (h: Equation14 G) : Equation23 G := by + intro x + calc + x + _ = (x ∘ x) ∘ (x ∘ (x ∘ x)) := (h x (x ∘ x)) + _ = (x ∘ x) ∘ x := by rw [← h x x] + +@[equational_result] +theorem Equation14_implies_Equation8 (G: Type*) [Magma G] (h: Equation14 G) : Equation8 G := by +intro x +calc + x + _ = x ∘ (x ∘ x) := h x x + +@[equational_result] +theorem Equation2_implies_Equation14 (G: Type*) [Magma G] (h: Equation2 G) : Equation14 G := by +intro x y +calc + x + _ = y ∘ (x ∘ y) := Eq.symm (h (y ∘ (x ∘ y)) x) + /- Counterexamples -/ @[equational_result] From 8cbe2eed1d2d1b1de9eb7eaa3edeb79265357eb9 Mon Sep 17 00:00:00 2001 From: Amir Livne Bar-on Date: Thu, 3 Oct 2024 01:04:36 +0300 Subject: [PATCH 3/3] extact_implications: add --equivalence_creators flag to unknowns subcommand (#197) * extact_implications: add --equivalence_creators flag to unknowns subcommand * add link to equivalence_creators.json to the readme, with statistics --- README.md | 1 + scripts/extract_implications.lean | 8 +++++++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index edbf5b62..0510ca3b 100644 --- a/README.md +++ b/README.md @@ -21,6 +21,7 @@ Some automatically generated progress: - Oct 2, 2024: All but 7999 implications were [conjecturally resolved using the vampire ATP](equational_theories/Generated/Vampire). Some statistics and data files from a given point in time: +- Oct 2, 2024: [A list of unknown implications whose converse is proven](https://github.com/amirlb/equational_theories/blob/extract_implications_equivalence_creators_data/scripts/equivalence_creators.json), i.e. implications that would reduce the number of equivalence classes of equations. At the time of creation we had 2969 equivalence classes. This file contains 4526 unknown implications, if all hold then it will reduce the number of equivalence classes to 1300. - 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. - Sep 29, 2024: [Here](https://leanprover.zulipchat.com/user_uploads/3121/7ImuNeVLCa_gIsS8bHYIsokB/direct.tar.xz) is a text file of the (21K or so) direct implications proven to date, and [here](https://leanprover.zulipchat.com/user_uploads/3121/wnbVe2BZ1gamFjlMYFE7sIs9/closure.tar.xz) is the transitive closure of these implications (about 4.5m). More precisely, we have 21791 implications explicitly proven true, 4494090 additional relations implicitly proven true, 739207 explicitly proven false, 12764328 implicitly proven false, one additional relations explicitly conjectured true (and 64 more implicitly conjectured true), and 4014155 remaining implications which remain completely open. Quotienting out by known equivalences, there are 3182453 open implications remaining. - Oct 2, 2024: 23019 implications explicitly proven true (and an additional 5925922 implicitly proven); 829607 explicitly proven false (and an additional 12994633 implicitly disproven); 38489 explicitly conjectured true (and an additional 1223057 implicitly conjectured), and 79635 explicitly conjectured false (and an additional 1540725 implicitly conjectured false). This only leads 7999 open implications! diff --git a/scripts/extract_implications.lean b/scripts/extract_implications.lean index 26dfff4c..b1f08aec 100644 --- a/scripts/extract_implications.lean +++ b/scripts/extract_implications.lean @@ -22,6 +22,7 @@ def withExtractedResults (imp : Cli.Parsed) (action : Array Entry → IO UInt32) action rs def generateUnknowns (inp : Cli.Parsed) : IO UInt32 := do + let only_e_c := inp.hasFlag "equivalence_creators" withExtractedResults inp fun rs => do let rs' := if inp.hasFlag "proven" then rs.filter (·.proven) else rs let rs' := rs'.map (·.variant) @@ -30,7 +31,11 @@ def generateUnknowns (inp : Cli.Parsed) : IO UInt32 := do for i in [:equations.size] do for j in [:equations.size] do if outcomes[i]![j]!.isNone then - unknowns := unknowns.push ⟨equations[i]!, equations[j]!⟩ + if only_e_c then + if outcomes[j]![i]!.getD false then + unknowns := unknowns.push ⟨equations[i]!, equations[j]!⟩ + else + unknowns := unknowns.push ⟨equations[i]!, equations[j]!⟩ IO.println (toJson unknowns).compress pure 0 @@ -40,6 +45,7 @@ def unknowns : Cmd := `[Cli| FLAGS: proven; "Only consider proven results" + equivalence_creators; "Output only implications whose converse is known to be true" ARGS: ...files : Array ModuleName; "The files to extract the implications from"