This is the first pass at annotating Achal Kumar's solution to the Putnam problem. Here we will not explore alternative runs, but mostly add notes with a little cleaning up. Some general observations:

  • Tangent provers were not used.
  • Most of the choices were instantiations and possibly dropping generation with operations.

A proof by identifying Lemmas

Let ⋆ be a binary operation on a nonempty set $M$. That is, every pair $(a,b) \in M$ is assigned an element $a$ ⋆$ b$ in $M$. Suppose that ⋆ has the additional property that $(a $ ⋆ $b) $ ⋆$ b= a$ and $a$ ⋆ $(a$ ⋆$ b)= b$ for all $a,b \in M$. Show that $a$ ⋆ $b = b$ ⋆ $a$ for all $a,b \in M$.

Here we try to solve the given problem by identifying the lemmas generated by the LocalProver. We can not add all the axioms in one single distribution because it would not be possible for the LocaProver to generate any relevant lemmas due to combinatorial explosion.

Thus we divide the whole set of axioms ,relevant with the proof into different parts, use the LocalProver on them to get a significant set of lemmas then create distribution which consist of the derrived lemmas and repeat the process until we get the desired result.

In the proof we would be generating following results :

  1. $ (m*n)*n= m $
  2. $ (m*n)*((m*n)*n) = n $
  3. $ ((m*n)*m) = (m*n)*((m*n)*n) $
  4. $ ((m*n)*m))*m = m*n $
  5. $ (m*n)*m = n $
  6. $ ((m*n)*m)*m = n*m $

These are the intermediate results that the prover proves and then using them finally proves the desired result

$ m*n = n*m $


In [1]:
import $cp.bin.`provingground-core-jvm-0b6bd9c864.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}


Out[1]:
import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 

In [2]:
import library._, MonoidSimple._


Out[2]:
import library._, MonoidSimple._

In [3]:
val M = "M" :: Type

val eqM = "eqM" :: M ->: M ->: Type

val a = "a" :: M
val b = "b" :: M
val c = "c" :: M

val m = "m" :: M

val n = "n" :: M

val op = "mul" :: M ->: M ->: M
val pl = "plus" :: M ->: M ->: M

import FineDeducer.unif


Out[3]:
M: Typ[Term] = M
eqM: Func[Term, Func[Term, Typ[Term]]] = eqM
a: Term = a
b: Term = b
c: Term = c
m: Term = m
n: Term = n
op: Func[Term, Func[Term, Term]] = mul
pl: Func[Term, Func[Term, Term]] = plus
import FineDeducer.unif

We have imported from the Monoid library, which has many things in common with the current problem.


In [4]:
val putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
    eqM(a)(a),
    eqM(a)(b) ->: eqM(b)(a),
    eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
    eqM(op(op(a)(b))(b))(a),
    eqM(op(a)(op(a)(b)))(b),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term) * 0.125) ++ (FiniteDistribution.unif(op : Term ) * 0.375)


Out[4]:
putn: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.041666666666666664),
    Weighted(b, 0.041666666666666664),
    Weighted(c, 0.041666666666666664),
    Weighted(m, 0.041666666666666664),
    Weighted(n, 0.041666666666666664),
    Weighted(mul, 0.041666666666666664),
    Weighted(eqM, 0.041666666666666664),
    Weighted(axiom_{eqM(a)(a)}, 0.041666666666666664),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.041666666666666664),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.041666666666666664
    ),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.041666666666666664),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.041666666666666664),
    Weighted(eqM, 0.125),
    Weighted(mul, 0.375)
  )
)

The above is the basic generating model. This has no instantiations. It is not actually used, but is kept here as it is the most canonical. We have removed t


In [5]:
private val t3putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op,op(m)(n), eqM)(
    eqM(a)(b) ->: eqM(b)(a),
    eqM(op(op(a)(b))(b))(a),
    eqM(op(a)(op(a)(b)))(b),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)

val t3putn1 = t3putn.filter((t) => !Set(a, b, c).contains(t)).normalized()


Out[5]:
t3putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.05263157894736841),
    Weighted(n, 0.05263157894736841),
    Weighted(mul, 0.05263157894736841),
    Weighted(mul(m)(n), 0.05263157894736841),
    Weighted(eqM, 0.05263157894736841),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
    Weighted(eqM, 0.28947368421052627),
    Weighted(mul, 0.28947368421052627)
  )
)

We make the first local prover with the above. This has symmetry for equality, but not transitivity or $ap_f$.


In [6]:
import monix.execution.Scheduler.Implicits.global
val ts = TermState(t3putn1,t3putn1.map(_.typ))
val lp = LocalProver(ts, cutoff = 0.000005).noIsles


Out[6]:
import monix.execution.Scheduler.Implicits.global

ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.05263157894736841),
      Weighted(n, 0.05263157894736841),
      Weighted(mul, 0.05263157894736841),
      Weighted(mul(m)(n), 0.05263157894736841),
      Weighted(eqM, 0.05263157894736841),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
      Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
      Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
      Weighted(eqM, 0.28947368421052627),
      Weighted(mul, 0.28947368421052627)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.05263157894736841),
      Weighted(M, 0.05263157894736841),
      Weighted((M → (M → M)), 0.05263157894736841),
      Weighted(M, 0.05263157894736841),
      Weighted((M → (M → 𝒰 )), 0.05263157894736841),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.05263157894736841
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
        0.05263157894736841
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
        0.05263157894736841
      ),
      Weighted((M → (M → 𝒰 )), 0.28947368421052627),
      Weighted((M → (M → M)), 0.28947368421052627)
    )
  ),
  Vector(),
...
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.05263157894736841),
        Weighted(n, 0.05263157894736841),
        Weighted(mul, 0.05263157894736841),
        Weighted(mul(m)(n), 0.05263157894736841),
        Weighted(eqM, 0.05263157894736841),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05263157894736841),
        Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.05263157894736841),
        Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.05263157894736841),
        Weighted(eqM, 0.28947368421052627),
        Weighted(mul, 0.28947368421052627)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.05263157894736841),
        Weighted(M, 0.05263157894736841),
        Weighted((M → (M → M)), 0.05263157894736841),
        Weighted(M, 0.05263157894736841),
        Weighted((M → (M → 𝒰 )), 0.05263157894736841),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.05263157894736841
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
          0.05263157894736841
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
          0.05263157894736841
        ),
        Weighted((M → (M → 𝒰 )), 0.28947368421052627),
        Weighted((M → (M → M)), 0.28947368421052627)
      )
    ),
...

We run this, synchronously for now, and get lemmas.


In [7]:
val lem = lp.lemmas.runSyncUnsafe()


Out[7]:
lem: Vector[(Typ[Term], Double)] = Vector(
  (eqM(n)(mul(m)(mul(m)(n))), 3.150279366819256E-4),
  (eqM(m)(mul(mul(m)(n))(n)), 2.7034870284010703E-4),
  (eqM(mul(mul(m)(n))(n))(m), 3.062988293669645E-5),
  (eqM(mul(m)(mul(m)(n)))(n), 3.062988293669645E-5),
  (eqM(mul(m)(n))(mul(n)(mul(n)(mul(m)(n)))), 1.2164940347298408E-5),
  (eqM(mul(m)(n))(mul(m)(mul(m)(mul(m)(n)))), 1.2164940347298408E-5),
  (
    eqM(mul(m)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(m)(n)))),
    1.2164940347298408E-5
  ),
  (eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.0614151718697937E-5),
  (eqM(n)(mul(n)(mul(n)(n))), 1.0614151718697937E-5),
  (eqM(m)(mul(n)(mul(n)(m))), 1.0614151718697937E-5),
  (eqM(m)(mul(m)(mul(m)(m))), 1.0614151718697937E-5),
  (eqM(m)(mul(mul(m)(n))(mul(mul(m)(n))(m))), 1.0614151718697937E-5)
)

At this stage we make a choice, picking the second and eighth lemma for use. Only the second is used immediately, so we would clearly not get stuck here.


In [8]:
import provingground.{FiniteDistribution => FD}
val x = "lemma1" :: lem(1)._1
val y = "lemma2" :: lem(7)._1
x.typ
y.typ


Out[8]:
import provingground.{FiniteDistribution => FD}

x: Term = lemma1
y: Term = lemma2
res7_3: Typ[U] = eqM(m)(mul(mul(m)(n))(n))
res7_4: Typ[U] = eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n)))

The lemmas we have picked are:

  • $lemma_1 : m = (m * n) * n$
  • $lemma_2 : n = (m * n) * ((m * n) * n)$

In [9]:
private val tputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
    eqM(b)(c) ->: eqM(op(a)(b))(op(a)(c))
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, x ,op(m)(n)) * 0.5)
val tputin1 = tputin.filter((t) => !Set(a, b, c).contains(t)).normalized()

val ts1 = TermState(tputin1,tputin1.map(_.typ), goals = FD.unif(eqM(op(op(m)(n))(m))( op(op(m)(n))(op(op(m)(n))(n)))))
val lp1 = LocalProver(ts1, cutoff = 0.000002).noIsles


Out[9]:
tputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.07692307692307693),
    Weighted(n, 0.07692307692307693),
    Weighted(mul, 0.07692307692307693),
    Weighted(eqM, 0.07692307692307693),
    Weighted(
      axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
      0.07692307692307693
    ),
    Weighted(eqM, 0.20512820512820512),
    Weighted(lemma1, 0.20512820512820512),
    Weighted(mul(m)(n), 0.20512820512820512)
  )
)
ts1: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.07692307692307693),
      Weighted(n, 0.07692307692307693),
      Weighted(mul, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(
        axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
        0.07692307692307693
      ),
      Weighted(eqM, 0.20512820512820512),
      Weighted(lemma1, 0.20512820512820512),
      Weighted(mul(m)(n), 0.20512820512820512)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.07692307692307693),
      Weighted(M, 0.07692307692307693),
      Weighted((M → (M → M)), 0.07692307692307693),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(a)(b))(mul(a)(c))) } } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.20512820512820512),
      Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.20512820512820512),
      Weighted(M, 0.20512820512820512)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(
      Weighted(eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.0)
    )
  ),
...
lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.07692307692307693),
        Weighted(n, 0.07692307692307693),
        Weighted(mul, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(
          axiom_{(eqM(b)(c) \to eqM(mul(a)(b))(mul(a)(c)))},
          0.07692307692307693
        ),
        Weighted(eqM, 0.20512820512820512),
        Weighted(lemma1, 0.20512820512820512),
        Weighted(mul(m)(n), 0.20512820512820512)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.07692307692307693),
        Weighted(M, 0.07692307692307693),
        Weighted((M → (M → M)), 0.07692307692307693),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(a)(b))(mul(a)(c))) } } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.20512820512820512),
        Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.20512820512820512),
        Weighted(M, 0.20512820512820512)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(
        Weighted(eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.0)
      )
...

We have set up our second local prover. This uses the lemma x, i.e. Lemma 1 and also transport of equality under left multiplication, but nothing else.


In [10]:
val lem2 = lp1.lemmas.runSyncUnsafe()


Out[10]:
lem2: Vector[(Typ[Term], Double)] = Vector(
  (
    eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
    0.9079462369542685
  ),
  (eqM(mul(n)(m))(mul(n)(mul(mul(m)(n))(n))), 1.0252535689104723E-5),
  (eqM(mul(m)(m))(mul(m)(mul(mul(m)(n))(n))), 1.0252535689104723E-5)
)

In [11]:
val z = "lemma3" :: lem2(0)._1
z.typ


Out[11]:
z: Term = lemma3
res10_1: Typ[U] = eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n)))

In this case z, i.e. Lemma 3 is the overwhelmingly dominant lemma, so natural to pick. It has type:

  • $lemma_3 : (m * n) * m = (m * n) * ((m * n) * n)$

In [12]:
private val tt2putn =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
 eqM(op(op(a)(b))(b))(a),
 eqM(op(a)(op(a)(b)))(b)
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op(m)(n)) * 0.5)
val tt2putn1 = tt2putn.filter((t) => !Set(a, b, c).contains(t)).normalized()

val ts2 = TermState(tt2putn1,tt2putn1.map(_.typ), goals = FD.unif(eqM(op(op(op(m)(n))(m))(m))(op(m)(n))))
val lp2 = LocalProver(ts2, cutoff = 0.00001).noIsles


Out[12]:
tt2putn1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.06666666666666667),
    Weighted(n, 0.06666666666666667),
    Weighted(mul, 0.06666666666666667),
    Weighted(eqM, 0.06666666666666667),
    Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.06666666666666667),
    Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.06666666666666667),
    Weighted(eqM, 0.3),
    Weighted(mul(m)(n), 0.3)
  )
)
ts2: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.06666666666666667),
      Weighted(n, 0.06666666666666667),
      Weighted(mul, 0.06666666666666667),
      Weighted(eqM, 0.06666666666666667),
      Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.06666666666666667),
      Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.06666666666666667),
      Weighted(eqM, 0.3),
      Weighted(mul(m)(n), 0.3)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06666666666666667),
      Weighted(M, 0.06666666666666667),
      Weighted((M → (M → M)), 0.06666666666666667),
      Weighted((M → (M → 𝒰 )), 0.06666666666666667),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
        0.06666666666666667
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
        0.06666666666666667
      ),
      Weighted((M → (M → 𝒰 )), 0.3),
      Weighted(M, 0.3)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 1.0))
  ),
  Empty
)
lp2: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.06666666666666667),
        Weighted(n, 0.06666666666666667),
        Weighted(mul, 0.06666666666666667),
        Weighted(eqM, 0.06666666666666667),
        Weighted(axiom_{eqM(mul(mul(a)(b))(b))(a)}, 0.06666666666666667),
        Weighted(axiom_{eqM(mul(a)(mul(a)(b)))(b)}, 0.06666666666666667),
        Weighted(eqM, 0.3),
        Weighted(mul(m)(n), 0.3)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06666666666666667),
        Weighted(M, 0.06666666666666667),
        Weighted((M → (M → M)), 0.06666666666666667),
        Weighted((M → (M → 𝒰 )), 0.06666666666666667),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(mul(a)(b))(b))(a) } },
          0.06666666666666667
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ eqM(mul(a)(mul(a)(b)))(b) } },
          0.06666666666666667
        ),
        Weighted((M → (M → 𝒰 )), 0.3),
        Weighted(M, 0.3)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 1.0))
    ),
    Empty
  ),
...

We set up the next local prover. This has no lemmas proved along the way, but is focussed on using the given axioms without any properties of equality.


In [13]:
val lem3 = lp2.lemmas.runSyncUnsafe()


Out[13]:
lem3: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.9036614962977492),
  (eqM(mul(mul(m)(n))(n))(m), 1.0248486491665673E-5)
)

We note that this ran quickly, and all it gave was an instantiation of one of the properties (as we would expect). We pick up another lemma.


In [14]:
val w = "lemma4" :: lem3(0)._1
w.typ


Out[14]:
w: Term = lemma4
res13_1: Typ[U] = eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n))

The lemma we have obtained is

  • $lemma_4 : ((m * n) * m) * m = m * n$
  • this is $(a * b) * b = a$ when $a = m * n$ and $b = m$.

In [15]:
val stputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
 eqM(a)(b) ->: eqM(b)(a),
 eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, x, y,z) * 0.5)
val stputin1 = stputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts4 = TermState(stputin1,stputin1.map(_.typ), goals = FD.unif(eqM(op(op(m)(n))(m))(n)) )
val lp4 = LocalProver(ts4, cutoff = 0.00001).noIsles


Out[15]:
stputin: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(a, 0.05555555555555555),
    Weighted(b, 0.05555555555555555),
    Weighted(c, 0.05555555555555555),
    Weighted(m, 0.05555555555555555),
    Weighted(n, 0.05555555555555555),
    Weighted(mul, 0.05555555555555555),
    Weighted(eqM, 0.05555555555555555),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.05555555555555555),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.05555555555555555
    ),
    Weighted(eqM, 0.125),
    Weighted(lemma1, 0.125),
    Weighted(lemma2, 0.125),
    Weighted(lemma3, 0.125)
  )
)
stputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.06666666666666667),
    Weighted(n, 0.06666666666666667),
    Weighted(mul, 0.06666666666666667),
    Weighted(eqM, 0.06666666666666667),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666667),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.06666666666666667
    ),
    Weighted(eqM, 0.15),
    Weighted(lemma1, 0.15),
    Weighted(lemma2, 0.15),
    Weighted(lemma3, 0.15)
  )
)
ts4: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.06666666666666667),
      Weighted(n, 0.06666666666666667),
      Weighted(mul, 0.06666666666666667),
      Weighted(eqM, 0.06666666666666667),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666667),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.06666666666666667
      ),
      Weighted(eqM, 0.15),
      Weighted(lemma1, 0.15),
      Weighted(lemma2, 0.15),
      Weighted(lemma3, 0.15)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06666666666666667),
      Weighted(M, 0.06666666666666667),
      Weighted((M → (M → M)), 0.06666666666666667),
      Weighted((M → (M → 𝒰 )), 0.06666666666666667),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.06666666666666667
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.06666666666666667
      ),
      Weighted((M → (M → 𝒰 )), 0.15),
      Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.15),
      Weighted(eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 0.15),
      Weighted(eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))), 0.15)
    )
  ),
...
lp4: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.06666666666666667),
        Weighted(n, 0.06666666666666667),
        Weighted(mul, 0.06666666666666667),
        Weighted(eqM, 0.06666666666666667),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666667),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.06666666666666667
        ),
        Weighted(eqM, 0.15),
        Weighted(lemma1, 0.15),
        Weighted(lemma2, 0.15),
        Weighted(lemma3, 0.15)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06666666666666667),
        Weighted(M, 0.06666666666666667),
        Weighted((M → (M → M)), 0.06666666666666667),
        Weighted((M → (M → 𝒰 )), 0.06666666666666667),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.06666666666666667
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.06666666666666667
        ),
        Weighted((M → (M → 𝒰 )), 0.15),
        Weighted(eqM(m)(mul(mul(m)(n))(n)), 0.15),
        Weighted(eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 0.15),
        Weighted(
          eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
...

We are looking for consequences of our first three lemmas. This should give the crucial Lemma 5.


In [16]:
val lemI = lp4.lemmas.runSyncUnsafe()


Out[16]:
lemI: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(mul(m)(n))(m))(n), 0.9085367798328954),
  (eqM(m)(m), 0.0057629510380071665),
  (eqM(n)(n), 0.0057629510380071665)
)

In [17]:
val lI = "lemma5" :: lemI(0)._1
lI.typ


Out[17]:
lI: Term = lemma5
res16_1: Typ[U] = eqM(mul(mul(m)(n))(m))(n)

We obtain a crucial lemma. Note that this is not instantiation.

  • $lemma_5 : (m * n) * m = n$

In [18]:
private val s2tputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(b)(c) ->: eqM(op(b)(a))(op(c)(a))
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, lI) * 0.5)
val s2tputin1 = s2tputin.filter((t) => !Set(a, b, c).contains(t)).normalized()

val ts5 = TermState(s2tputin1,s2tputin1.map(_.typ), goals = FD.unif(eqM(op(op(op(m)(n))(m))(m))(op(n)(m))))
val lp5 = LocalProver(ts5, cutoff = 0.00001).noIsles


Out[18]:
s2tputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.07692307692307693),
    Weighted(n, 0.07692307692307693),
    Weighted(mul, 0.07692307692307693),
    Weighted(eqM, 0.07692307692307693),
    Weighted(
      axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))},
      0.07692307692307693
    ),
    Weighted(eqM, 0.3076923076923077),
    Weighted(lemma5, 0.3076923076923077)
  )
)
ts5: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.07692307692307693),
      Weighted(n, 0.07692307692307693),
      Weighted(mul, 0.07692307692307693),
      Weighted(eqM, 0.07692307692307693),
      Weighted(
        axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))},
        0.07692307692307693
      ),
      Weighted(eqM, 0.3076923076923077),
      Weighted(lemma5, 0.3076923076923077)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.07692307692307693),
      Weighted(M, 0.07692307692307693),
      Weighted((M → (M → M)), 0.07692307692307693),
      Weighted((M → (M → 𝒰 )), 0.07692307692307693),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(b)(a))(mul(c)(a))) } } },
        0.07692307692307693
      ),
      Weighted((M → (M → 𝒰 )), 0.3076923076923077),
      Weighted(eqM(mul(mul(m)(n))(m))(n), 0.3076923076923077)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(
    Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 1.0))
  ),
  Empty
)
lp5: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.07692307692307693),
        Weighted(n, 0.07692307692307693),
        Weighted(mul, 0.07692307692307693),
        Weighted(eqM, 0.07692307692307693),
        Weighted(
          axiom_{(eqM(b)(c) \to eqM(mul(b)(a))(mul(c)(a)))},
          0.07692307692307693
        ),
        Weighted(eqM, 0.3076923076923077),
        Weighted(lemma5, 0.3076923076923077)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.07692307692307693),
        Weighted(M, 0.07692307692307693),
        Weighted((M → (M → M)), 0.07692307692307693),
        Weighted((M → (M → 𝒰 )), 0.07692307692307693),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(b)(c) → eqM(mul(b)(a))(mul(c)(a))) } } },
          0.07692307692307693
        ),
        Weighted((M → (M → 𝒰 )), 0.3076923076923077),
        Weighted(eqM(mul(mul(m)(n))(m))(n), 0.3076923076923077)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(
      Vector(Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 1.0))
    ),
    Empty
  ),
  TermGenParams(
...

We setup yet another local prover. Here we are looking for consequences of Lemma 5, which was just discovered.


In [19]:
val lemI1 = lp5.lemmas.runSyncUnsafe()


Out[19]:
lemI1: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.9002505096459986)
)

In [20]:
val lI1 = "lemma6" :: lemI1(0)._1
lI1.typ


Out[20]:
lI1: Term = lemma6
res19_1: Typ[U] = eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m))

Note that the above ran almost instantly. The lemma we obtained is:

  • $lemma_6 : ((m * n) * m) * m = n * m $

In [21]:
private val finalstputin =  FineDeducer.unif(a,b,c)(m,n,op, eqM)(
 eqM(a)(b) ->: eqM(b)(a),
 eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
  ) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, w, lI1) * 0.5)
val finalstputin1 = finalstputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts5 = TermState(finalstputin1,finalstputin1.map(_.typ), goals = FD.unif(eqM(op(m)(n))(op(n)(m))))
val lp5 = LocalProver(ts5, cutoff = 0.00001).noIsles


Out[21]:
finalstputin1: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(m, 0.06666666666666668),
    Weighted(n, 0.06666666666666668),
    Weighted(mul, 0.06666666666666668),
    Weighted(eqM, 0.06666666666666668),
    Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666668),
    Weighted(
      axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
      0.06666666666666668
    ),
    Weighted(eqM, 0.2),
    Weighted(lemma4, 0.2),
    Weighted(lemma6, 0.2)
  )
)
ts5: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(m, 0.06666666666666668),
      Weighted(n, 0.06666666666666668),
      Weighted(mul, 0.06666666666666668),
      Weighted(eqM, 0.06666666666666668),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666668),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.06666666666666668
      ),
      Weighted(eqM, 0.2),
      Weighted(lemma4, 0.2),
      Weighted(lemma6, 0.2)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.06666666666666668),
      Weighted(M, 0.06666666666666668),
      Weighted((M → (M → M)), 0.06666666666666668),
      Weighted((M → (M → 𝒰 )), 0.06666666666666668),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.06666666666666668
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.06666666666666668
      ),
      Weighted((M → (M → 𝒰 )), 0.2),
      Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.2),
      Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.2)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
...
lp5: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(m, 0.06666666666666668),
        Weighted(n, 0.06666666666666668),
        Weighted(mul, 0.06666666666666668),
        Weighted(eqM, 0.06666666666666668),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.06666666666666668),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.06666666666666668
        ),
        Weighted(eqM, 0.2),
        Weighted(lemma4, 0.2),
        Weighted(lemma6, 0.2)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.06666666666666668),
        Weighted(M, 0.06666666666666668),
        Weighted((M → (M → M)), 0.06666666666666668),
        Weighted((M → (M → 𝒰 )), 0.06666666666666668),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.06666666666666668
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.06666666666666668
        ),
        Weighted((M → (M → 𝒰 )), 0.2),
        Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.2),
        Weighted(eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.2)
      )
    ),
    Vector(),
...

We set up our final step. This uses Lemmas 4 and 6 from earlier.


In [22]:
lp5.lemmas.runSyncUnsafe()


Out[22]:
res21: Vector[(Typ[Term], Double)] = Vector(
  (eqM(mul(m)(n))(mul(n)(m)), 0.9118516347852311)
)

This is the conclusion.