Merge branch 'main' of https://github.com/teorth/equational_theories

README.md

@@ -21,6 +21,7 @@ Some automatically generated progress:
 - 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:
+- 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!

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]

home_page/_layouts/default.html

@@ -30,7 +30,7 @@ <h2 class="project-tagline">{{ page.description | default: site.description | de
     <a href="blueprint" class="btn">Blueprint (web)</a>
     <a href="blueprint.pdf" class="btn">Blueprint (pdf)</a>
     <a href="docs" class="btn">Documentation</a>
-    <a href="{{site.baseurl}}/dashboard" class="btn">Dashboard</a>
+    <a href="{{site.url}}/dashboard" class="btn">Dashboard</a>
     {% if site.github.is_project_page %}
     <a href="{{ site.github.repository_url }}" class="btn">GitHub</a>
     {% endif %}

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"