## Stream: Machine Learning for Theorem Proving

### Topic: Generate similar but not equal type

#### Joachim Hauge (May 08 2021 at 11:34):

Given a type A the task is to find a type B and maps f:A->B, g:B->A minimizing the sum of lengths of f and g. You are also not allowed to pick B=A.

So in logical terms the task is to find a statement different from a given statement but that is transparently logically equivalent to it.

Is there a program that can solve this task? Were similar things considered in the literature?

#### Kevin Buzzard (May 08 2021 at 12:00):

I choose B = id A

#### Joachim Hauge (May 08 2021 at 12:02):

Kevin Buzzard said:

I choose B = id A

Does id mean the identity on the universe? That's judgmentally equal to A. I meant you aren't allowed to pick judgmentally equal things.

#### Kevin Buzzard (May 08 2021 at 12:03):

Ok I choose the subtype of option A corresponding to A

#### Joachim Hauge (May 08 2021 at 12:10):

OK I don't know all the details of Lean's pattern matching. Let's say you are only allowed to use Pi-types, Sigma-types, the natural numbers, axiom choice and law of excluded middle. Can you still trivialize this game?

#### Shing Tak Lam (May 08 2021 at 12:12):

Doesn't B = unit -> A work?

#### Joachim Hauge (May 08 2021 at 12:22):

Shing Tak Lam said:

Doesn't B = unit -> A work?

It does. OK as stated this game is nonsense. I think there maybe a fix via homotopy type theory (have two players where one player can shoot down the proposals (B, f, g) of the other if they can exhibit an equivalence h:A->B of similar length).

#### Kevin Buzzard (May 08 2021 at 12:43):

In homotopy type theory if f and g are inverses then I'm afraid B = A by the univalence axiom!

#### Joachim Hauge (May 08 2021 at 13:12):

Kevin Buzzard said:

In homotopy type theory if f and g are inverses then I'm afraid B = A by the univalence axiom!

No in the homotopy version we would allow A=B but we would impose an upper limit on the lengths of the definitions of the equivalences (e.g. any provable proposition is equal to 1 but the length of the minimum equivalence can be large).

#### Jason Rute (May 09 2021 at 10:32):

@Joachim Hauge what is the motivation for this game?

#### Joachim Hauge (May 09 2021 at 10:42):

Jason Rute said:

Joachim Hauge what is the motivation for this game?

No particular motivation. I am just trying to think of ways to make reinforcement learning algorithms think non-trivial thoughts other than "here is a statement, prove or disprove it".

Last updated: Dec 20 2023 at 11:08 UTC