Autoformalization

Stream: lean4

[David Afonso Valente]

Hi! I'm aware that autoformalization isn't the main topic of interest however it seems like it would be great to have a reliable way to transate NL to FP seen as we would be able to generate a lot more data to train a F2F prover given all of the NL proofs available. Another possible use case I can think of is this would allow us to formally check NL proofs which would also greatly benefit Inf2Inf solutions and potentialy aid a hybrid solution in which we take advantadge of LLMs' impresive reasoning abilities. I am curious to know other peoples opinion on this matter.

[Mario Carneiro]

You should probably check out #Machine Learning for Theorem Proving which has a bunch of discussions related to this