Week 12: Miscellanea

The pieces that fit nowhere else: the Solitaire applet, the shortest Principia proofs, open problems, where the community talks, meetings, a video, the GitHub organisation, and one paragraph of history.

24 May 2027

The last lecture collects the pieces that fit under no earlier week.

Metamath Solitaire is a Java applet, downloadable from the home page as mmsolitaire.zip. In Wiedijk’s survey Megill says “a unification algorithm lets the user know exactly what possibilities are available at any point in a proof”, and that it “is not practical for larger proofs” (PDF, p. 104).

The shortest Principia proofs. pmproofs.txt holds proofs of “all 193 theorems of propositional calculus” in Principia Mathematica from ax-1, ax-2, ax-3 and ax-mp, in a notation the file calls condensed detachment. Its revision history runs from Gregory Bush’s 2004 shortening of 67 proofs to Samiro Discher’s 2025 shortening of 38 with pmGenerator.

Open problems. The workshop miscellany page “was originally created as part of a presentation at the 2003 Argonne Workshop on Automated Reasoning and Deduction”; “Items 2 through 17 each present one or more open problems (which in some cases have been solved, as noted)”. Item 9 asks whether Metamath’s predicate-calculus axioms are independent.

Where people talk. “The Metamath Google Group mailing list is a great place to discuss Metamath” (home page; the group). The site’s other page also lists a Gitter chat room “set up by Mario Carneiro”.

Meetings. Megill’s Institut Henri Poincaré slides of 9 May 2014 open with “Very small verifier (≈300 lines code)”. The other page records Big Proof 2017, where “Mario Carneiro presents Metamath in the first part of this talk”, and FOMM 2020, held at Carnegie Mellon from 6 to 10 January 2020, where Carneiro’s talk was “Metamath Zero, or: How to Verify a Verifier” (other.html).

The record, drawn. “Metamath Proof Explorer (set.mm) contributions visualized with Gource through 2019-10-04” is a video on the same page.

The organisation. github.com/metamath was created on 11 September 2013 and holds, among others, metamath-exe, “source code for the Metamath executable”, and set.mm.

History. The set.mm README dedicates the collection to the memory of Norman “Norm” Dwight Megill, Ph.D. (1950-2021), “creator of the Metamath system and cultivator of an international community of people with the shared dream of digitizing and formally verifying mathematics”.

Read#

• pmproofs.txt — the header, for how a proof fits in seven characters.
• Workshop miscellany — open problems you can now state.
• IHP 2014 slides — the language on one slide, from its author.