Starting with just types, we will seek top unknowns as goals.

import $cp.bin.`provingground-core-jvm-a6ae52a.fat.jar`

import $cp.$                                           

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

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

repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}

val terms = FiniteDistribution.unif[Term](Type, Unit, Zero, Star)
val typs = FiniteDistribution.unif[Typ[Term]](Type, Unit, Zero)
val ts = TermState(terms, typs)

terms: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted(𝒰 , 0.25),
    Weighted(Unit, 0.25),
    Weighted(Zero, 0.25),
    Weighted(Star, 0.25)
  )
)
typs: FiniteDistribution[Typ[Term]] = FiniteDistribution(
  Vector(
    Weighted(𝒰 , 0.3333333333333333),
    Weighted(Unit, 0.3333333333333333),
    Weighted(Zero, 0.3333333333333333)
  )
)
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.25),
      Weighted(Unit, 0.25),
      Weighted(Zero, 0.25),
      Weighted(Star, 0.25)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(𝒰 , 0.3333333333333333),
      Weighted(Unit, 0.3333333333333333),
      Weighted(Zero, 0.3333333333333333)
    )
  ),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)

import monix.execution.Scheduler.Implicits.global
val lp = LocalProver(ts).sharpen(10)
val thmsT = lp.theoremsByStatement 
val thmsF = thmsT.runToFuture

import monix.execution.Scheduler.Implicits.global

lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.25),
        Weighted(Unit, 0.25),
        Weighted(Zero, 0.25),
        Weighted(Star, 0.25)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(𝒰 , 0.3333333333333333),
        Weighted(Unit, 0.3333333333333333),
        Weighted(Zero, 0.3333333333333333)
      )
    ),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.1,
    0.1,
    0.1,
    0.05,
    0.05,
    0.05,
    0.0,
    0.0,
    0.0,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
...
thmsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Map(
  FlatMap(
    Map(
      Async(<function2>, false, true, true),
      provingground.learning.LocalProver$$Lambda$2760/368487092@670c538f,
      0
    ),
    provingground.learning.LocalProver$$Lambda$2761/1658847093@473b622e
  ),
  provingground.learning.LocalProverStep$$Lambda$2762/303319596@364600a4,
  0
)
thmsF: monix.execution.CancelableFuture[FiniteDistribution[Typ[Term]]] = Success(
  FiniteDistribution(
    Vector(
      Weighted((Zero → (𝒰  → Unit)), 3.0497390746605195E-4),
      Weighted((Zero → (Zero → Unit)), 4.356770106657885E-4),
      Weighted((Zero → (Unit → Unit)), 4.356770106657885E-4),
      Weighted((𝒰  → (Zero → Unit)), 2.688606639440138E-4),
      Weighted((𝒰  → (𝒰  → Unit)), 1.8820246476080962E-4),
      Weighted((𝒰  → (Unit → Unit)), 2.688606639440138E-4),
      Weighted(∏(@a : 𝒰 ){ (@a → Unit) }, 3.4567799649944635E-4),
      Weighted((Unit → (Unit → Unit)), 4.3567701066578866E-4),
      Weighted((Unit → (Zero → Unit)), 4.3567701066578866E-4),
      Weighted((Unit → (𝒰  → Unit)), 3.04973907466052E-4),
      Weighted(𝒰 , 0.41378006453846056),
      Weighted(Unit×𝒰 , 0.006307547629305582),
      Weighted((𝒰  → Unit), 0.009476178164047663),
      Weighted((Zero → Unit), 0.015196691774522063),
      Weighted((𝒰 ×Zero → Unit), 1.6475595324836717E-4),
      Weighted(((Zero → Unit) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → Unit) → Unit), 2.886934634346448E-4),
      Weighted((∑(@a : { @a } → Unit), 2.1182908274790062E-4),
      Weighted((Unit×Zero → Unit), 2.0476811332297058E-4),
      Weighted((Unit×Unit → Unit), 2.0476811332297058E-4),
      Weighted((Zero×𝒰  → Unit), 2.0476811332297058E-4),
      Weighted((Zero×Unit → Unit), 2.0476811332297058E-4),
      Weighted((𝒰 ×𝒰  → Unit), 1.6475595324836717E-4),
      Weighted(((Zero → Zero) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → Zero) → Unit), 2.886934634346448E-4),
      Weighted((Unit → Unit), 0.01650481911361812),
      Weighted((Unit×𝒰  → Unit), 2.0476811332297058E-4),
      Weighted(((Unit → Unit) → Unit), 3.873991333137281E-4),
      Weighted(((Unit → Zero) → Unit), 3.873991333137281E-4),
      Weighted((Zero×Zero → Unit), 2.0476811332297058E-4),
      Weighted(((Zero → 𝒰 ) → Unit), 3.873991333137281E-4),
      Weighted(((𝒰  → 𝒰 ) → Unit), 2.474515400868384E-4),
      Weighted(((Unit → 𝒰 ) → Unit), 2.905493499852961E-4),
      Weighted((𝒰 ×Unit → Unit), 1.6475595324836717E-4),
      Weighted((∏(@a : 𝒰 ){ @a } → Unit), 3.7117731013025767E-4),
      Weighted(∑(@a : { @a }, 0.005079885089552229),
...

val unknownsT = lp.unknownStatements.map(_.entropyVec.map(_.elem)).memoize
val unF = unknownsT.runToFuture

unknownsT: monix.eval.Task[Vector[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)
unF: monix.execution.CancelableFuture[Vector[Typ[Term]]] = Success(
  Vector(
    ∏(@a : 𝒰 ){ @a },
    (Unit → (Unit → Zero)),
    (Zero → ∏(@a : 𝒰 ){ @a }),
    (Unit → ∏(@a : 𝒰 ){ @a }),
    (𝒰  → ∏(@b : 𝒰 ){ @b }),
    ∏(@a : 𝒰 ){ (Zero → @a) },
    ∏(@a : 𝒰 ){ (Unit → @a) },
    (Unit → (𝒰  → Zero)),
    ∏(@a : (Unit → 𝒰 )){ @a(Star) },
    (𝒰  → (Unit → Zero)),
    ∏(@a : 𝒰 ){ @a×@a },
    ∑(@a : { (@a → @a) },
    ∏(@a : 𝒰 ){ (𝒰  → @a) },
    (Unit → Unit×Zero),
    (Zero → Unit×Zero),
    (Unit → Zero×𝒰 ),
    (Zero → Zero×𝒰 ),
    (Unit → Unit×𝒰 ),
    (Zero → Unit×𝒰 ),
    (Zero → Zero×Zero),
    (Unit → Zero×Zero),
    (Zero → Zero×Unit),
    (Unit → Zero×Unit),
    (Unit → Unit×Unit),
    (Zero → Unit×Unit),
    (Zero → ∑(@a : { @a }),
    (Unit → ∑(@a : { @a }),
    (Zero×Unit → Zero),
    (Zero×𝒰  → Zero),
    (Unit×Zero → Zero),
    (Zero×Zero → Zero),
    (𝒰  → ∑(@b : { @b }),
    ∏(@a : 𝒰 ){ @a×𝒰  },
    ∏(@a : 𝒰 ){ @a×Zero },
    ∏(@a : 𝒰 ){ @a×Unit },
    ∏(@a : 𝒰 ){ Zero×@a },
    ∏(@a : 𝒰 ){ Unit×@a },
...

def seekGoals(typ: Typ[Term]) = lp.addGoals(typ -> 0.5, negate(typ) -> 0.5).successes

defined function seekGoals

def topGoals(n: Int) = (0 until n).map{j => unknownsT.flatMap(v => seekGoals(v(j)))}

defined function topGoals

val top20 = topGoals(20)
top20.map(_.runToFuture)

top20: collection.immutable.IndexedSeq[monix.eval.Task[Vector[(Typ[Term], Double, FiniteDistribution[Term])]]] = Vector(
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@2d492f74
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@7e3c63c4
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@120460a6
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@7ffc7409
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@27a2b914
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@3a9dcc67
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@bad8ac2
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@17edfb82
  ),
  FlatMap(
    Async(<function2>, false, true, true),
    ammonite.$sess.cmd12$Helper$$Lambda$3573/1199703190@25359a72
  ),
  FlatMap(
...
res13_1: collection.immutable.IndexedSeq[monix.execution.CancelableFuture[Vector[(Typ[Term], Double, FiniteDistribution[Term])]]] = Vector(
  Success(
  Vector(
    (
      ∑(@a : { (@a → Zero) },
      0.5,
      FiniteDistribution(
        Vector(
          Weighted((Zero , rec_{ Zero ; Zero }), 0.009912434376452174),
          Weighted((Zero , (@a : Zero) ↦ @a), 0.009912434376452174)
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ((Unit → (Unit → Zero)) → Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (@a : (Unit → (Unit → Zero))) ↦ @a(Star)(Star),
            0.0191661641766036
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      (Zero → ∏(@a : 𝒰 ){ @a }),
      0.5,
      FiniteDistribution(
        Vector(Weighted(rec_{ Zero ; ∏(@a : 𝒰 ){ @a } }, 0.02524248658291313))
      )
    )
  )
),
  Success(
  Vector(
    (
      ((Unit → ∏(@a : 𝒰 ){ @a }) → Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (@a : (Unit → ∏(@a : 𝒰 ){ @a })) ↦ @a(Star)(Zero),
            0.0191661641766036
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ((𝒰  → ∏(@b : 𝒰 ){ @b }) → Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (@a : (𝒰  → ∏(@b : 𝒰 ){ @b })) ↦ @a(Unit)(Zero),
            0.0095830820883018
          ),
          Weighted(
            (@a : (𝒰  → ∏(@b : 𝒰 ){ @b })) ↦ @a(Zero)(Zero),
            0.0095830820883018
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ∏(@a : 𝒰 ){ (Zero → @a) },
      0.5,
      FiniteDistribution(
        Vector(Weighted((@a : 𝒰 ) ↦ rec_{ Zero ; @a }, 0.02216424605959186))
      )
    )
  )
),
  Success(
  Vector(
    (
      ∑(@a : { ((Unit → @a) → Zero) },
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (Zero , (@a : (Unit → Zero)) ↦ @a(Star)),
            0.01982316937709552
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ((Unit → (𝒰  → Zero)) → Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (@a : (Unit → (𝒰  → Zero))) ↦ @a(Star)(Zero),
            0.0095830820883018
          ),
          Weighted(
            (@a : (Unit → (𝒰  → Zero))) ↦ @a(Star)(Unit),
            0.0095830820883018
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ∑(@a : { (@a(Star) → Zero) },
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            ((@a : Unit) ↦ Zero , rec_{ Zero ; Zero }),
            0.004946099629479799
          ),
          Weighted(
            ((@a : Unit) ↦ Zero , (@a : Zero) ↦ @a),
            0.004946099629479799
          ),
          Weighted(
            (rec_{ Unit ; 𝒰  }(Zero) , (@a : Zero) ↦ @a),
            0.004946099629479799
          ),
          Weighted(
            (rec_{ Unit ; 𝒰  }(Zero) , rec_{ Zero ; Zero }),
            0.004946099629479799
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ((𝒰  → (Unit → Zero)) → Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (@a : (𝒰  → (Unit → Zero))) ↦ @a(Unit)(Star),
            0.0095830820883018
          ),
          Weighted(
            (@a : (𝒰  → (Unit → Zero))) ↦ @a(Zero)(Star),
            0.0095830820883018
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ∑(@a : { (@a → Zero) + (@a → Zero) },
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(
            (Zero , FirstIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),rec(Zero)(Zero))),
            0.005120352121428702
          ),
          Weighted(
            (Zero , ScndIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),rec(Zero)(Zero))),
            0.005120352121428702
          ),
          Weighted(
            (Zero , ScndIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),(`@a :  Zero) ↦ (`@a))),
            0.004791232567119057
          ),
          Weighted(
            (Zero , FirstIncl(PlusTyp((Zero) → (Zero),(Zero) → (Zero)),(`@a :  Zero) ↦ (`@a))),
            0.004791232567119057
          )
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ∑(@a : { (@a → @a) },
      0.5,
      FiniteDistribution(
        Vector(
          Weighted((Unit , rec_{ Unit ; Unit }(Star)), 0.004946499273937881),
          Weighted((Zero , (@a : Zero) ↦ @a), 0.004946499273937881),
          Weighted((Zero , rec_{ Zero ; Zero }), 0.004946499273937881),
          Weighted((Unit , (@a : Unit) ↦ @a), 0.0031241048045923467),
          Weighted((Unit , (@a : Unit) ↦ Star), 0.0018223944693455355)
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      ∑(@a : { ((𝒰  → @a) → Zero) },
      0.5,
      FiniteDistribution(
        Vector(
          Weighted((Zero , (@a : (𝒰  → Zero)) ↦ @a(Unit)), 0.00991158468854776),
          Weighted((Zero , (@a : (𝒰  → Zero)) ↦ @a(Zero)), 0.00991158468854776)
        )
      )
    )
  )
),
  Success(Vector()),
  Success(
  Vector(
    (
      (Zero → Unit×Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(rec_{ Zero ; Unit×Zero }, 0.017091576549434707),
          Weighted((@a : Zero) ↦ (Star , @a), 0.0104964584462948)
        )
      )
    )
  )
),
  Success(Vector()),
  Success(
  Vector(
    (
      (Zero → Zero×𝒰 ),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted((@a : Zero) ↦ (@a , Zero), 0.005238463685229454),
          Weighted(rec_{ Zero ; Zero×𝒰  }, 0.01709191390737606),
          Weighted((@a : Zero) ↦ (@a , Unit), 0.005238463685229454)
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      (Unit → Unit×𝒰 ),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted((@a : Unit) ↦ (@a , Zero), 0.003189116089034762),
          Weighted(rec_{ Unit ; Unit×𝒰  }((Star , Zero)), 0.004755330860038047),
          Weighted((@a : Unit) ↦ (@a , Unit), 0.003189116089034762),
          Weighted(rec_{ Unit ; Unit×𝒰  }((Star , Unit)), 0.004755330860038047),
          Weighted((@a : Unit) ↦ (Star , Unit), 0.001860317718603611),
          Weighted((@a : Unit) ↦ (Star , Zero), 0.001860317718603611)
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      (Zero → Unit×𝒰 ),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted((@a : Zero) ↦ (Star , Zero), 0.005238463685229454),
          Weighted((@a : Zero) ↦ (Star , Unit), 0.005238463685229454),
          Weighted(rec_{ Zero ; Unit×𝒰  }, 0.01709191390737606)
        )
      )
    )
  )
),
  Success(
  Vector(
    (
      (Zero → Zero×Zero),
      0.5,
      FiniteDistribution(
        Vector(
          Weighted(rec_{ Zero ; Zero×Zero }, 0.017091576549434714),
          Weighted((@a : Zero) ↦ (@a , @a), 0.010496458446294802)
        )
      )
    )
  )
)
)

While a very modest task, this has been a success in both workflow and results.