Questions on proof assistants

[dennis at logicalphalluses.net]

To add to Freek Wiedijk's email:

> Examples of projects like this are Joe Hurd's OpenTheory,
> and Gilles Dowek's Dedukti/Logipedia, but I'm sure there
> are a lot more.

There is also my Ph.D. thesis on that problem "Mathematical Knowledge 
Management Across Formal Libraries" in the MMT ecosystem: 
https://kwarc.info/people/dmueller/pubs/thesis.pdf

Best

-- 
Dennis M. Müller
"Mathematics is the music of reason. To do mathematics is to engage in an act of discovery and conjecture, intuition and inspiration; to be in a state of confusion— not because it makes no sense to you, but because you gave it sense and you still don’t understand what your creation is up to; to have a breakthrough idea; to be frustrated as an artist; to be awed and overwhelmed by an almost painful beauty; to be alive, damn it. Remove this from mathematics and you can have all the conferences you like; it won’t matter. Operate all you want, doctors: your patient is already dead."
  - Paul Lockhart (on mathematics in school)