Proof assistant
Software tool to assist with the development of formal proofs by human–machine collaboration / From Wikipedia, the free encyclopedia
For verification in computer science, see formal verification.
For the academic conference, see Interactive Theorem Proving (conference).
Not to be confused with Interactive proof system.
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.
This article is missing information about automated proof checking. (February 2024) |
This article includes a list of general references, but it lacks sufficient corresponding inline citations. (November 2018) |
A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.[1]