(“증명 보조기 Proof Assistant” 2024)
- 2024 "증명 보조기 Proof assistant" 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.
Related-Notes
- [Terence Tao (2024) Machine Assisted Proof #형식증명]
References
“증명 보조기 Proof Assistant.” 2024. In Wikipedia. https://en.wikipedia.org/w/index.php?title=Proof_assistant&oldid=1226931114.