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.
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.