<div dir="ltr"><div><div><div><div>Hi OpenTheory list!<br><br></div>I have a question about the fundamental proof representation format used by OpenTheory:<br><br>Why not lambda terms?<br><br>I am inspired by the proof terms available in the Isabelle theorem prover. If one reads Berghofer and Nipkow's work on proof terms, they recount a number of reasons to prefer lambda terms to a flat unstructured sequence of commands for a virtual machine. Mostly these advantages come in the form of being able to re-use results from areas such as type checking and term rewriting more easily in the compression of proofs. (Apart from technical reasons, there are probably also social reasons for making things appealing to a wide group of smart people.)<br><br></div>Now, it may be that in practice these supposed advantages of proof terms don't show up. Was the OpenTheory design chosen after a careful comparison, or was it just a matter of using something familiar and straightforward?<br><br></div>Cheers,<br></div>Ramana<br></div>