Comment by lairv

That could only generate constructivist [0] proofs, and there are many things done in modern maths which are not constructivist. Maybe a better approach would be to use Curry-Howard [1] correspondence to directly get proofs from generated programs

[0] https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_...

[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...