 | 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) |
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.
A recent effort within this field is making these tools use artificial intelligence to automate the formalization of ordinary mathematics.[1]
- ^ Ornes, Stephen (August 27, 2020). "Quanta Magazine – How Close Are Computers to Automating Mathematical Reasoning?".