Metamath 100... would love to see more

David A. Wheeler

unread,

Dec 4, 2016, 8:38:31 PM12/4/16

to meta...@googlegroups.com

I'd love to see more completed entries on the metamath 100 list:
http://us.metamath.org/mm_100.html

Currently metamath has proven 58; the next higher are Coq (63) and Mizar (64):
http://www.cs.ru.nl/%7Efreek/100/

It would only take 5 more to tie with Coq!

--- David A.Wheeler

Mario Carneiro

unread,

Dec 4, 2016, 11:10:00 PM12/4/16

to metamath

Any thoughts on particular achievable goals among the remaining 42?

--- David A.Wheeler
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

David A. Wheeler

unread,

Dec 4, 2016, 11:38:23 PM12/4/16

to metamath, metamath

On Sun, Dec 4, 2016 at 8:38 PM, David A. Wheeler wrote:
> > I'd love to see more completed entries on the metamath 100 list:
> > http://us.metamath.org/mm_100.html

On Sun, 4 Dec 2016 23:09:58 -0500, Mario Carneiro <di....@gmail.com> wrote:
> Any thoughts on particular achievable goals among the remaining 42?

Let's agree that #33, Fermat's Last Theorem, isn't where to start :-).

A few that seem especially ripe to me are:
9. The Area of a Circle
47. The Central Limit Theorem
53. π is Transcendental
55. Product of Segments of Chords
64. L'Hôpital's Rule
65. Isosceles Triangle Theorem
67. e is Transcendental
97. Cramer's Rule
100. Descartes Rule of Signs

The full list of "not done by Metamath" is also at http://us.metamath.org/mm_100.html

--- David A. Wheeler

fl

unread,

Dec 5, 2016, 5:48:47 AM12/5/16

to Metamath, dwhe...@dwheeler.com

A few that seem especially ripe to me are:
9. The Area of a Circle

It depends on what theory you take to define the concept of circle. If one is kind

enough to give me the time I'll give the proof beginning by the definition of

a circle in Euclid's planar geometry.

Enough time means one year.

--

FL

Thierry Arnoux

unread,

Dec 5, 2016, 8:09:29 AM12/5/16

to meta...@googlegroups.com

Hi all,

I've been working on a proof for

30. The Ballot Problem

recently. The inductive proof would have been the easiest way, but I'm
trying myself at the more elegant reflection method...
_
Thierry

Norman Megill

unread,

Dec 5, 2016, 9:05:56 AM12/5/16

to Metamath

On Sunday, December 4, 2016 at 11:10:00 PM UTC-5, Mario Carneiro wrote:

Any thoughts on particular achievable goals among the remaining 42?

As a crude measure of "achievable", it might be interesting to look at which of these 42 have the most proofs done in the other proof languages.

Norm

David A. Wheeler

unread,

Dec 5, 2016, 11:08:27 PM12/5/16

to metamath, Metamath

On Mon, 5 Dec 2016 06:05:56 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> As a crude measure of "achievable", it might be interesting to look at
> which of these 42 have the most proofs done in the other proof languages.

Fair point. Done.

Below is a list of the "Formalizing 100 Theorems" list from
<http://www.cs.ru.nl/~freek/100/> which have *not* been formalized by Metamath,
sorted by the count of the number of other systems which *have* formalized a proof.
The leader by far is Taylor's Theorem (his theorem #35); this has been formalized
by 7 provers, including ACL2 and PVS, but not with Metamath. This is followed by L'Hopital's Rule.

Given this, I'd love to know if anyone hopes to pick up any of them soon...!

Here's the full list (I list the number of provers first):

7 35. Taylor's Theorem
5 64. L'Hôpital's Rule
4 97. Cramer's Rule
4 96. Principle of Inclusion/Exclusion
4 65. Isosceles Triangle Theorem
4 6. Gödel's Incompleteness Theorem
4 30. The Ballot Problem
3 9. The Area of a Circle
3 84. Morley's Theorem
3 83. The Friendship Theorem
3 61. Theorem of Ceva
3 57. Heron's Formula
3 55. Product of Segments of Chords
3 49. The Cayley-Hamilton Theorem
3 45. The Partition Theorem
3 36. Brouwer Fixed Point Theorem
3 13. Polyhedron Formula
3 100. Descartes Rule of Signs
2 90. Stirling's Formula
2 8. The Impossibility of Trisecting the Angle and Doubling the Cube
2 67. e is Transcendental
2 40. Minkowski's Fundamental Theorem
2 29. Feuerbach's Theorem
2 28. Pascal's Hexagon Theorem
2 12. The Independence of the Parallel Postulate
1 99. Buffon Needle Problem
1 92. Pick's Theorem
1 76. Fourier Series
1 53. Pi is Transcendental
1 50. The Number of Platonic Solids
1 47. The Central Limit Theorem
1 41. Puiseux's Theorem
1 32. The Four Color Problem
1 21. Green's Theorem
0 82. Dissection of Cubes (J.E. Littlewood's "elegant" proof)</li>
0 62. Fair Games Theorem</li>
0 59. The Laws of Large Numbers</li>
0 56. The Hermite-Lindemann Transcendence Theorem</li>
0 43. The Isoperimetric Theorem</li>
0 33. Fermat's Last Theorem</li>
0 24. The Undecidability of the Continuum Hypothesis</li>
0 16. Insolvability of General Higher Degree Equations</li>

Below is the source code of the quick program I created to generate this.

--- David A. Wheeler

==================================

#!/usr/bin/python
# by David A. Wheeler

# First, do:
# curl -o freek.html http://www.cs.ru.nl/~freek/100/
# Then run as:
# ./count.py | sort -nr

# Try to hide Python 2/3 differences. For more, see:
# http://www.dwheeler.com/essays/python3-in-python2.html
from __future__ import print_function, unicode_literals
from __future__ import absolute_import, division
try:
xrange = xrange
# We have Python 2
except:
xrange = range
# We have Python 3

# Use regular expressions to extract info
import re
proof_re = re.compile(r'<li id="([0-9]*)">(.*)')

provers = [ 'HOL Light', 'Isabelle', 'Mizar', 'Coq', 'Metamath',
'ProofPower', 'nqthm', 'ACL2', 'PVS', 'NuPRL']

name = [ '' for x in xrange(101) ] # Name for given id#

results = [ {} for x in xrange(101) ]

before_list = 1

def show_report(rows):
for counter, row in enumerate(rows):
if counter > 0 and 'Metamath' not in row:
print(str(len(row)) + "\t" + str(counter) + ". " + name[counter])

# Process lines
with open('freek.html') as f:
for line in f:
if before_list and '<li id="1">' in line: # List begun?
before_list = 0
if not before_list and 'has some obvious omissions.' in line: # end?
break
if before_list: # Skip stuff before list begin.
continue
find_id = proof_re.search(line)
if find_id != None:
id = int(find_id.group(1))
# print(find_id.group(2))
name[id] = find_id.group(2)
for prover in provers:
if prover in line:
results[id][prover] = 1

# print(results)
show_report(results)

Mario Carneiro

unread,

Dec 6, 2016, 12:42:56 AM12/6/16

to metamath

Taylor's theorem is definitely the closest to current formalization in Metamath, since it requires essentially no major foundation-building that many of the others require, and the proof itself is not much more complicated than the FTC, which we have had for some time. I am currently busy with grad school, and my slow-burn Metamath project is getting ENF up and running, but after that I'll see if I can work on Taylor's theorem.

Mario

David A. Wheeler

unread,

Dec 7, 2016, 9:06:04 PM12/7/16

to meta...@googlegroups.com, Mario Carneiro

On December 6, 2016 12:42:54 AM EST, Mario Carneiro <di....@gmail.com> wrote:
>Taylor's theorem is definitely the closest to current formalization in
>Metamath, since it requires essentially no major foundation-building
>that
>many of the others require, and the proof itself is not much more
>complicated than the FTC, which we have had for some time.

Are there any that have "obvious foundations needed"? Which ones don't need anything more?

Maybe we can identify some foundations that are obvious next steps, and then build a roadmap. For example, I think these have common foundations that are needed first:

>> 2 67. e is Transcendental

>> 1 53. Pi is Transcendental

--- David A.Wheeler

David A. Wheeler

unread,

Dec 7, 2016, 9:49:16 PM12/7/16

to meta...@googlegroups.com, Mario Carneiro

On December 6, 2016 12:42:54 AM EST, Mario Carneiro <di....@gmail.com> wrote:

>Taylor's theorem is definitely the closest to current formalization in

>Metamath, since it requires essentially no major foundation-building...

Which of the top 7 most common proofs need serious foundations?:

>> 7 35. Taylor's Theorem
>> 5 64. L'Hôpital's Rule
>> 4 97. Cramer's Rule
>> 4 96. Principle of Inclusion/Exclusion
>> 4 65. Isosceles Triangle Theorem
>> 4 6. Gödel's Incompleteness Theorem
>> 4 30. The Ballot Problem

--- David A.Wheeler

fl

unread,

Dec 8, 2016, 7:49:50 AM12/8/16

to Metamath, di....@gmail.com

>> 4 6. Gödel's Incompleteness Theorem

This one. You must formalize the idea of logic.

--

FL

Norman Megill

unread,

Dec 9, 2016, 8:14:09 AM12/9/16

to Metamath

An arxiv article posted just yesterday includes a summary of 6 different proofs. It may be helpful towards selecting one to formalize.

https://arxiv.org/abs/1612.02549

Norm

David A. Wheeler

unread,

Dec 10, 2016, 3:25:17 PM12/10/16

to metamath, Metamath

On Wed, Dec 7, 2016 at 9:48 PM, David A. Wheeler <dwhe...@dwheeler.com>

> Which of the top 7 most common proofs need serious foundations?:

On Fri, 9 Dec 2016 05:14:09 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> An arxiv article posted just yesterday includes a summary of 6 different

> proofs. It may be helpful towards selecting one to formalize (Goedel's).
> https://arxiv.org/abs/1612.02549

To make the info easier to find/concentrate, I've created GitHub issues
for each of these 7 "most common proofs", to make it easier for people to learn
that these need doing & put (in one place) hints about how to do them.

Here are the counts of other formalization tools, the metamath 100 number, name, and URL for the GitHub issue:
* 7 35. Taylor's Theorem
https://github.com/metamath/set.mm/issues/83
* 5 64. L'Hôpital's Rule
https://github.com/metamath/set.mm/issues/84
* 4 97. Cramer's Rule
https://github.com/metamath/set.mm/issues/85
* 4 96. Principle of Inclusion/Exclusion
https://github.com/metamath/set.mm/issues/86
* 4 65. Isosceles Triangle Theorem
https://github.com/metamath/set.mm/issues/40 (this was already there)
* 4 6. Gödel's Incompleteness Theorem
https://github.com/metamath/set.mm/issues/87
* 4 30. The Ballot Problem
https://github.com/metamath/set.mm/issues/88

If you have hints about how to do them - or are working on them - let everyone know!

--- David A. Wheeler

David A. Wheeler

unread,

Dec 10, 2016, 7:19:40 PM12/10/16

to meta...@googlegroups.com

Mario will see if he can work on Taylor's theorem, I hope to try again on the isosceles triangle theorem, and we have a volunteer for the ballot problem. Anyone willing to try any of the other ones?

--- David A.Wheeler

Reply all

Reply to author

Forward