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 b

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_mathematics) https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_... [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...