Home |
Software |
Publications |
Various |
Contact Us
# Replaying Flyspeck

We have employed our Common HOL
HOL Light proof exporter to export the main text formalisation of Flyspeck as
proof modules (directories of proof object files). These proof modules can be
imported into HOL Zero and HOL SuperLight
(our cut-down version of HOL Light, involving just its core system) using our
Common HOL proof importer extensions. The proof modules conform to version 0.5
of the Common HOL standard.

### Instructions for Importing the Proof

Download and unpack an import-adapted HOL Zero or HOL Light, to act as a
target system:

holzero-0.6.3.alpha2.tgz
and/or
holsuperlight-svn197.tgz

Create a proof repository directory to hold the proof modules.

Download the translation file, and place it in the proof repository
directory:

HOL_TRANS_TABLE

Download the following 17 proof module tarballs, and place the unpacked
directories in the proof repository directory:

BaseSystem.tgz (3Mb)
Multivariate.tgz (42Mb)
Start.tgz (7Mb)
TrigNonlinear.tgz (6Mb)
Volume.tgz (0.5Mb)
Hypermap.tgz (1.1Mb)
Fan.tgz (8Mb)
Packing.tgz (23Mb)
Local1.tgz (9Mb)
Tame1.tgz (4Mb)
Local2.tgz (7Mb)
Local3.tgz (11Mb)
Local4.tgz (13Mb)
Local5.tgz (9Mb)
Tame2.tgz (6Mb)
Tame3.tgz (8Mb)
End.tgz (1.7Mb)

The final theorem of the Flyspeck main text formalisation is called
`kepler_conjecture_with_assumptions`

.

To import Flyspeck into HOL Zero, first install and start a HOL
Zero session (see the README for instructions), then use the file
`FLYSPECK_IMPORT.ml`

(from the HOL Zero home directory) in the
HOL Zero session.

To import Flyspeck into HOL SuperLight, first install and start a HOL
SuperLight session (see the README for instructions), then use the file
`FLYSPECK_IMPORT.ml`

(from the `CommonHOL`

directory)
in the HOL SuperLight session.