[FOM] Proof assistants and conjectures

[Gergely Buday]

Timothy Chow writes:

> Someone claims to
> have a proof of the Riemann hypothesis, and even claims that some standard
> proof assistant has checked the proof.  If the claimant is free to
> formulate his or her own version of the Riemann hypothesis, then there
> would still be the possibility for debate about whether the claimant's
> formal theorem is, in fact, the Riemann hypothesis.  This loophole could
> be largely closed if there is a published, "official" version of the
> Riemann hypothesis than any wannabe millionaire needs to prove.

Different theorem provers can have different underlying logic and even
if the logic is similar the concrete syntax might be different. There
is a tool I know of though to reuse proofs - and so theorems - in
another system: one can import HOL4 proofs into Isabelle/HOL. The
authors of this method write:

---
In contrast to previous work is also that our translation is basically
between systems, not between logics. Although some complications
result from the fact that Isabelle/HOL is an object logic instance of
the Isabelle framework, and HOL 4 and HOL-light directly implement
higher-order logic, all these systems still share the same logic:
classical simply-typed polymorphic higher-order logic (HOL).
---

See http://www4.in.tum.de/~obua/importer/

But this is rather an exception, I do not know of any other conversion
package available (which might be my fault). Creating software that
operates between systems using different logics seems to be a
challenge.

> However, from the point of view of knowledge management, it would seem
> desirable to put down some stakes in the sand even in uncharted territory,
> to prevent different pioneers from developing overly idiosyncratic
> dialects that later turn out to be extremely difficult to translate
> between.

I'm afraid the dialects are already there: Coq, PVS, Mizar, HOL,
Isabelle etc so this cannot be called "uncharted territory". There are
the OpenMath and MathML communities though, see

http://www.openmath.org/overview/om-mml.html

but these are not picked up by theorem prover developers as far as I
know. There is some OpenMath software for GAP and Mathematica.

Best Wishes

- Gergely