https://lawrencecpaulson.github.io/2022/09/14/Libraries.html

[utterances-bot]

Porting Libraries of Mathematics Between Proof Assistants

https://lawrencecpaulson.github.io/2022/09/14/Libraries.html

[GergelyBuday]

What do you think of the Dedukti project for interoperability of proof assistants?

[lawrencecpaulson]

I know very little about it. From that little my impression is that it looks at proofs from a very low level. That means it may be able to tell you that a certain statement is a theorem—because it has been proved in some other system—but without being able to give you a proof you could understand.

[CoghettoR]

while we researchers should eat our own dog food, we shouldn’t force it on others.

😃