Replaying Flyspeck

Proof Technologies Ltd > Flyspeck

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.