we should collaborate

Stream: Machine Learning for Theorem Proving

[(deleted)]

I feel the space of test time strategies hasn't been explored and we are wasting the potential of LLMs. Really, empirically speaking I can paste a problem statement with a non rigorous hint and then the LLM can spit out a very strong argument that then can be subsequently formalized. And coming up with a strategy so that the LLM can do the formalization, I think should be feasible.

[Kelly Davis]

Essentially this technique has been used in at least Goedel-Prover-V2 and in DeepSeek-Prover-V2.

In Goedel-Prover-V2, Section 2.2 subsection Informal-based scaffolded data synthesis, it's used to create new formal (purported ) theorems at training time. In addition another variation is used at test time in Goedel-Prover-V2 to correct proofs, see for example Figure 9 the "Ours" row.

In DeepSeek-Prover-V2, Section 2.1 subsection Sketching Formal Proofs from Natural Language Reasoning, it's used at training time to create formal postulates whose proofs (purportedly) lead to the proof of the desired formal theorem.