Monoid in an automatic mode¶

We return to the old problem of proving $e_l = e_r$, but in a general autonomous/interactive framework.

import $cp.bin.`provingground-core-jvm-8e93db2c2a.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}


Utils.logger = {
    import scribe._, writer._, Utils._
    logger.withHandler(writer = FileWriter().path(file.LogPath.simple("monoid.log"))).replace()
}

import $cp.$                                              

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

import library._, MonoidSimple._
val tg = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)
val ts = TermState(dist1, dist1.map(_.typ), goals = FiniteDistribution.unif(eqM(l)(r)))
val lp = LocalProver(ts, tg)

import library._, MonoidSimple._

tg: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e_l, 0.047619047619047616),
      Weighted(e_r, 0.047619047619047616),
      Weighted(mul, 0.047619047619047616),
      Weighted(eqM, 0.047619047619047616),
      Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.047619047619047616
      ),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
      Weighted(eqM, 0.2857142857142857),
      Weighted(mul, 0.2857142857142857)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.047619047619047616),
      Weighted(M, 0.047619047619047616),
      Weighted((M → (M → M)), 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.047619047619047616),
      Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.047619047619047616
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.047619047619047616
      ),
      Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.2857142857142857),
      Weighted((M → (M → M)), 0.2857142857142857)
...
lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e_l, 0.047619047619047616),
        Weighted(e_r, 0.047619047619047616),
        Weighted(mul, 0.047619047619047616),
        Weighted(eqM, 0.047619047619047616),
        Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.047619047619047616
        ),
        Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
        Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
        Weighted(eqM, 0.2857142857142857),
        Weighted(mul, 0.2857142857142857)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.047619047619047616),
        Weighted(M, 0.047619047619047616),
        Weighted((M → (M → M)), 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.047619047619047616),
        Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.047619047619047616
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.047619047619047616
        ),
        Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
        Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.2857142857142857),
...

We have set up the ingredients for the statement and proof. We next create a session with the set of bots we actually need. The crucial choice here is to limit the generation to applications and unified applications. The other restrictions should not matter much.

import HoTTBot._

val bs = Vector(lpLemmas, scaleSplitLemmas(1), lemmaTangents(), lptToTermResult, termResultToFinalState, reportSuccesses)
val sess = new HoTTWebSession(bots = bs)

import HoTTBot._


bs: Vector[TypedPostResponse[_1, HoTTPostWeb, (Int, Int)] forSome { type _1 >: HoTTMessages.FinalState with (TermState, Set[EquationNode]) with LocalTangentProver with HoTTMessages.UseLemma with HoTTMessages.Lemmas with LocalProver <: Product with Serializable with Object }] = Vector(
  MicroBot(
    provingground.learning.HoTTBot$$$Lambda$2691/975941609@6b0effc0,
    provingground.learning.TypedPostResponse$MicroBot$$$Lambda$2689/1407547031@72eda1a6
  ),
  MiniBot(
    provingground.learning.HoTTBot$$$Lambda$2692/1366091899@43316df9,
    provingground.learning.MiniBot$$$Lambda$2613/558251617@37569396
  ),
  MicroBot(
    provingground.learning.HoTTBot$$$Lambda$2693/319436178@2733e6a6,
    provingground.learning.TypedPostResponse$MicroBot$$$Lambda$2689/1407547031@72eda1a6
  ),
  MicroBot(
    provingground.learning.HoTTBot$$$Lambda$2702/1189645419@713eacd0,
    provingground.learning.TypedPostResponse$MicroBot$$$Lambda$2689/1407547031@72eda1a6
  ),
  MicroBot(
    provingground.learning.TypedPostResponse$MicroBot$$$Lambda$2688/157269246@39a849ab,
    provingground.learning.TypedPostResponse$MicroBot$$$Lambda$2689/1407547031@72eda1a6
  ),
  Callback(
    provingground.learning.TypedPostResponse$Callback$$$Lambda$2705/1496786662@3ae1a72b,
    provingground.learning.TypedPostResponse$Callback$$$Lambda$2706/347237838@25f6007
  )
)
sess: HoTTWebSession = provingground.learning.HoTTWebSession@4b33bd05

Finally, we post to our session to get stuff started.

sess.post(lp, Set())

res3: concurrent.Future[PostData[_, HoTTPostWeb, (Int, Int)]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  PostData(
    LocalProver(
      TermState(
        FiniteDistribution(
          Vector(
            Weighted(e_l, 0.047619047619047616),
            Weighted(e_r, 0.047619047619047616),
            Weighted(mul, 0.047619047619047616),
            Weighted(eqM, 0.047619047619047616),
            Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
            Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
            Weighted(
              axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
              0.047619047619047616
            ),
            Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
            Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
            Weighted(eqM, 0.2857142857142857),
            Weighted(mul, 0.2857142857142857)
          )
        ),
        FiniteDistribution(
          Vector(
            Weighted(M, 0.047619047619047616),
            Weighted(M, 0.047619047619047616),
            Weighted((M → (M → M)), 0.047619047619047616),
            Weighted((M → (M → 𝒰 )), 0.047619047619047616),
            Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
            Weighted(
              ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
              0.047619047619047616
            ),
            Weighted(
              ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
              0.047619047619047616
            ),
            Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
...

Utils.reportText

res4: String = Success: Vector((((eqM) (e_l)) (e_r),1.0,[(((((axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}) (e_l)) (((mul) (e_l)) (e_r))) (e_r)) (lemma:((eqM) (e_l)) (((mul) (e_l)) (e_r)))) ((axiom_{eqM(mul(e_l)(a))(a)}) (e_r)) : 0.001024170092306373]))

Success: Running the above after just a few seconds gives the report of success.

Logs¶

We include by copy-paste the log files (included from the file). Note the success statement.

2020.05.25 10:23:24 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.LocalProver], id: (1,-1349507052), content:
LocalProver(TermState([eqM : 0.2857142857142857, mul : 0.2857142857142857, e_l : 0.047619047619047616, e_r : 0.047619047619047616, mul : 0.047619047619047616, eqM : 0.047619047619047616, axiom_{eqM(a)(a)} : 0.047619047619047616, axiom_{(eqM(a)(b) \to eqM(b)(a))} : 0.047619047619047616, axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))} : 0.047619047619047616, axiom_{eqM(mul(e_l)(a))(a)} : 0.047619047619047616, axiom_{eqM(mul(a)(e_r))(a)} : 0.047619047619047616],[(M) → ((M) → (𝒰 _0)) : 0.2857142857142857, (M) → ((M) → (M)) : 0.2857142857142857, M : 0.047619047619047616, M : 0.047619047619047616, (M) → ((M) → (M)) : 0.047619047619047616, (M) → ((M) → (𝒰 _0)) : 0.047619047619047616, (`a : M ) ~> (((eqM) (`a)) (`a)) : 0.047619047619047616, (`a : M ) ~> ((`b : M ) ~> ((((eqM) (`a)) (`b)) → (((eqM) (`b)) (`a)))) : 0.047619047619047616, (`a : M ) ~> ((`b : M ) ~> ((`c : M ) ~> ((((eqM) (`a)) (`b)) → ((((eqM) (`b)) (`c)) → (((eqM) (`a)) (`c)))))) : 0.047619047619047616, (`a : M ) ~> (((eqM) (((mul) (e_l)) (`a))) (`a)) : 0.047619047619047616, (`a : M ) ~> (((eqM) (((mul) (`a)) (e_r))) (`a)) : 0.047619047619047616],Vector(),[],[((eqM) (e_l)) (e_r) : 1.0],Empty),TermGenParams(0.1,0.1,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.0,0.3,0.7,0.5,0.0,0.0,0.0,<function1>),1.0E-4,None,12 minutes,1.01,1.0,10000,10,1.0,1.0,None,false,false,0.5,1.0)
2020.05.25 10:23:24 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalProver], id: (1,-1349507052)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Lemmas], id: (2,1419581202), content:
Lemmas(Vector((((eqM) (e_r)) (e_r),None,0.0027509184472828325), (((eqM) (e_l)) (e_l),None,0.0027509184472828325), (((eqM) (e_l)) (((mul) (e_l)) (e_r)),None,0.0012526844961492322), (((eqM) (e_l)) (((mul) (e_l)) (e_l)),None,0.0012526844961492322), (((eqM) (e_r)) (((mul) (e_l)) (e_r)),None,0.0012526844961492322), (((eqM) (e_r)) (((mul) (e_r)) (e_r)),None,0.0012526844961492322)))
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Lemmas], id: (2,1419581202)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Weight], id: (3,-397054148), content:
Weight(0.26167884451748746)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Weight], id: (8,-1403795547), content:
Weight(0.1191605777412563)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (9,-897240716), content:
UseLemma(((eqM) (e_r)) (e_r),None)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Weight], id: (7,-1403795547), content:
Weight(0.1191605777412563)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Weight], id: (6,-1403795547), content:
Weight(0.1191605777412563)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Weight], id: (4,-397054148), content:
Weight(0.26167884451748746)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.Weight], id: (5,-1403795547), content:
Weight(0.1191605777412563)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (13,-1470620296), content:
UseLemma(((eqM) (e_l)) (e_l),None)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (14,774457819), content:
UseLemma(((eqM) (e_l)) (((mul) (e_l)) (e_r)),None)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (12,1349890185), content:
UseLemma(((eqM) (e_l)) (((mul) (e_l)) (e_l)),None)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (11,-1419946672), content:
UseLemma(((eqM) (e_r)) (((mul) (e_l)) (e_r)),None)
2020.05.25 10:23:28 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (10,1179944372), content:
UseLemma(((eqM) (e_r)) (((mul) (e_r)) (e_r)),None)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (9,-897240716)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (13,-1470620296)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (14,774457819)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (12,1349890185)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (11,-1419946672)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.UseLemma], id: (10,1179944372)
2020.05.25 10:23:29 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (15,-2097001952)
2020.05.25 10:23:28 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (16,1481277112)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (15,-2097001952)
2020.05.25 10:23:29 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (16,1481277112)
2020.05.25 10:23:28 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (17,1299211175)
2020.05.25 10:23:29 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (17,1299211175)
2020.05.25 10:23:28 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (18,1615518517)
2020.05.25 10:23:28 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (18,1615518517)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (19,1838221781)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (19,1838221781)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (20,61122141)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.LocalTangentProver], id: (20,61122141)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (21,-293827785)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (21,-293827785)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (22,-1739022371)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (22,-1739022371)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (23,388473380)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (23,388473380)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (24,1105488446)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (25,1560009545)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (24,1105488446)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.$anonfun:76:22 - Success: Vector((((eqM) (e_l)) (e_r),1.0,[(((((axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}) (e_l)) (((mul) (e_l)) (e_r))) (e_r)) (lemma:((eqM) (e_l)) (((mul) (e_l)) (e_r)))) ((axiom_{eqM(mul(e_l)(a))(a)}) (e_r)) : 0.001024170092306373]))
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (25,1560009545)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (26,-1452315895)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (26,-1452315895)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (27,-1331912611)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (27,-1331912611)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (28,-625764359)
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (28,-625764359)
2020.05.25 10:23:32 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (29,-174381781)
2020.05.25 10:23:32 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (29,-174381781)
2020.05.25 10:23:32 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (30,586935838)
2020.05.25 10:23:32 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (30,586935838)
2020.05.25 10:23:32 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (31,-997289120)
2020.05.25 10:23:32 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (31,-997289120)
2020.05.25 10:23:32 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (32,931037492)
2020.05.25 10:23:32 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (32,931037492)

To higlight, here is the success statement again:

2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.$anonfun:76:22 - Success: Vector((((eqM) (e_l)) (e_r),1.0,[(((((axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}) (e_l)) (((mul) (e_l)) (e_r))) (e_r)) (lemma:((eqM) (e_l)) (((mul) (e_l)) (e_r)))) ((axiom_{eqM(mul(e_l)(a))(a)}) (e_r)) : 0.001024170092306373]))
2020.05.25 10:23:30 [INFO] provingground.learning.HoTTBot.scribeLog:691:16 - Post; tag: TypeTag[provingground.learning.TermData.TermResult], id: (25,1560009545)
2020.05.25 10:23:30 [INFO] provingground.learning.ErasablePostBuffer.$anon.post:85:22 - Post; tag: TypeTag[provingground.learning.HoTTMessages.FinalState], id: (26,-1452315895)

Conclusions¶

The simple result is proved in an autonomous way.
The main tuning is sticking to applications and unified applications and keeping parameters at reasonable values, including the scaling for tangents.