Flyspeck

From MathWeb

Jump to: navigation, search

Formally proving Kepler's conjecture (homepage see below)

Case study

Long-term goal: support Flyspeck in SWiM
Both SWiM and Semantic MediaWiki have been evaluated for their support for Flyspeck. On top of Semantic MediaWiki, we have prototyped a bit more.

Steps working here:

The “master source” is a large Twelf file (e.g. this one with definitions from trigonometry), manually annotated with a few wiki-specific metadata (topical categorization)
upload this file into the wiki (using a special page; sources)
1. The upload handler breaks the file down into fragments and for each Twelf fragment creates
  - one page only containing the Twelf code (with its mathematical document type annotated and symbols linked to the place of their declaration in the wiki). This page is overwritten on subsequent uploads.
  - one page including the Twelf formalization and a LaTeX representation, leaving additional space for manual annotations. This page is never overwritten. These pages are categorized by topic according to metadata given in the
  - So far, no LaTeX is generated automatically. For a few pages (Flyspeck/lemma-1-11, Flyspeck/lemma-1-3-a, Flyspeck/lemma-1-3-b, Flyspeck/lemma-1-4, and Flyspeck/lemma-1-7), LaTeX sources from the Flyspeck book have been added manually. Soon, it will also be possible to obtain a LaTeX representation of the Twelf formalization automatically.
Browse, query, search, annotate :-)

Overview

Container pages including Twelf formalizations, human-readable LaTeX (possibly), and manual annotations:

Symbols: Flyspeck/!, Flyspeck/*, Flyspeck/-, Flyspeck//, Flyspeck/ bar-, Flyspeck/ gt, Flyspeck/ lt, Flyspeck/ plus, Flyspeck/ til, Flyspeck/arccos, Flyspeck/arcsin, Flyspeck/arctan, Flyspeck/cos, Flyspeck/o, Flyspeck/one, Flyspeck/pi, Flyspeck/pow, Flyspeck/real', Flyspeck/sin, Flyspeck/sqr, Flyspeck/sqrt, Flyspeck/tan, Flyspeck/tm, Flyspeck/tp, and Flyspeck/zero
Definitions: Flyspeck/ gt-def, Flyspeck/ lt-def, and Flyspeck/real-def
Lemmas: Flyspeck/lemma-1-1, Flyspeck/lemma-1-11, Flyspeck/lemma-1-2-a, Flyspeck/lemma-1-2-b, Flyspeck/lemma-1-3-a, Flyspeck/lemma-1-3-b, Flyspeck/lemma-1-4, Flyspeck/lemma-1-5, Flyspeck/lemma-1-7, and Flyspeck/lemma-1-8

All these lists are generated automatically by inline queries.

Note about the features used:

All symbols are linked to their declaration/definition
All pages can be exported. (The format is not nice, but with a script, it should be easy to adapt.)

Query results: “all proven lemmas with a Twelf formalization”

Flyspeck/lemma-1-11

(source code: <ask format="ul">[[Category:Proven]] [[Category:Lemma]] [[written in::Twelf]]</ask> – Note that the query syntax will change in the next release of Semantic MediaWiki!)