AlphaProof trusted tester programme (discussion)

Stream: Machine Learning for Theorem Proving

[Eric Wieser]

Discussion thread for the AlphaProof trusted tester programme

[Kim Morrison]

(interesting questions in the registration form! Can't wait to see what gets implemented.)

[Emily Riehl]

I thought so too, though I wanted to select multiple answers several times!

[Emily Riehl]

I'm curious whether the current version of AlphaProof has the capacity to

1. Attempt to autoformalize definitions?

Eg a lot of theorems in category theory are of the form
theorem some_construction_exists : Nonempty (NameOfType) := sorry
so in practice AlphaProof would have to construct
def some_construction : NameOfType := sorry
If successful the def is more useful than the theorem, so it would be great to be able to work directly with the definition.

2. Use previous results in a Lean file (either with proofs or with sorries) to prove later results in that same file?