Skip to main content
15 votes

High-performance proof assistants

We have to distinguish two kinds of concurrency here: Concurrency when checking a single proof object, implemented within the proof assistant, as supported by e.g. Coq and Lean. Concurrency while ...
Clément's user avatar
  • 251
9 votes

High-performance proof assistants

Rolling with Clément's distinction of concurrency, there is a third one: Concurrency when doing proof search and/or finding counter examples. Isabelle supports all three kinds of concurrency. ...
Wno-all's user avatar
  • 1,118

Only top scored, non community-wiki answers of a minimum length are eligible