How To Access Elaborated Lean Proof Objects

Stream: lean4

[zmkm]

In theorem proving in lean book https://lean-lang.org/theorem_proving_in_lean4/introduction.html it is written that

"In fact, most such systems provide fully elaborated "proof objects" that can be communicated to other systems and checked independently."

How to access such proof objects, and any documentation on how the communication to external systems and checking is done?

[Henrik Böving]

In general they are accessed through meta programming. For systems not written in Lean they can also be exported by https://github.com/leanprover/lean4export into a standartized format

[Kyle Miller]

From within Lean, you can also see proof objects via the #print command, like

set_option pp.all -- this is optional
#print yourThmName

This isn't for communication with external checkers however. I thought I'd mention it in case you had not seen that the fully-elaborated proof objects are accessible for inspection.