I know there has been a lot of work in automated theorem proving.
I'm curious if anyone here is able to describe the state of the art in that. Is it really just a toy for basic things right now, or how realistic is it that we'd ever get to a point where the author of a paper like this could use a formal language to show that their proof is indeed valid and complete?
I'm curious if anyone here is able to describe the state of the art in that. Is it really just a toy for basic things right now, or how realistic is it that we'd ever get to a point where the author of a paper like this could use a formal language to show that their proof is indeed valid and complete?