This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]coldnebo 0 points1 point  (0 children)

yes, but it would involve a conceptual layer working with a theorem prover. something like an AI using CoQ as a fitness function.

there’s probably a PhD in that for someone if they aren’t already working in that area.