Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: A Complete Proof of the Robbins...

view this post on Zulip Email Gateway (Aug 18 2022 at 15:21):

From: Tobias Nipkow <nipkow@in.tum.de>
In 1996, Bill McCune's solved the Robbins Conjecture with the help of an
automatic theorem prover http://www.cs.unm.edu/~mccune/papers/robbins/.
Matthew Wampler-Doty has formalized the complete proof (not the proof
search!) in Isabelle/HOL:

A Complete Proof of the Robbins Conjecture
Matthew Wampler-Doty

This document gives a formalization of the proof of the Robbins
conjecture, following A. Mann, A Complete Proof of the Robbins
Conjecture, 2003.

http://afp.sourceforge.net/entries/Robbins-Conjecture.shtml

Last updated: Apr 19 2024 at 08:19 UTC