I would like to know if there are any proof formats which is used to exchange proofs among proof assistants. I realize different proof assistants use different foundations but for those that have the same or similar foundations are there any standard formats?
The OpenTheory system has a standard format for the core HOL logics supported by HOL Light, HOL4, ProofPower and HOL Zero.
There's also Metamath Zero by Mario Carneiro
There is also the TPTP format for theorem prover problems. It acts as a pretty standard format for stating results in a "prover independent" manner.