[rpois]

Does this formalization process include giving it the answer it should try to prove?

[Smaug123]

Nope, per Oliver Nash who worked on the thing: https://news.ycombinator.com/item?id=41070372