There are thousands of math theorems, since Euclide's books on geometry, written 2300 years ago, to the latest issue of "Annals of Mathematics". Wouldn't it be awesome to search theorems from the DDG homepage?

Wait man, are you going to seat in your garage collecting all theorems since mathematics was born? It would take some time...

No! it's already done! Read on.

Since the invention of automated theorem provers and proof assistants,

http://en.wikipedia.org/wiki/Automated_t...

http://en.wikipedia.org/wiki/Proof_assis...

a lot of effort have been put into writing statements and proofs of theorems in a machine readable form, and there are huge libraries already availables. Nonetheless, proof assistants has been constantly improved, leading to a better understanding of mathematics. Some of the major softwares are

http://en.wikipedia.org/wiki/Coq

http://en.wikipedia.org/wiki/HOL_Light

As of today, some of the brightest matematicians in the world are working on the "formalization" of the proofs of the Kepler Conjecture

http://mathworld.wolfram.com/KeplerConje...

and the classification of the finite simple groups.

http://en.wikipedia.org/wiki/Finite_simp...

The four colors theorem was formalized in 2005

http://en.wikipedia.org/wiki/Four_color_...

We are now at the point where a field medalist like Vladimir Voevodsky

http://en.wikipedia.org/wiki/Vladimir_Vo...

opened a github repo

https://github.com/vladimirias/Foundatio...

and started hacking!

Moreover, something happened in 2006: the need of transporting theorems from a system to another led to this paper,

http://www.springerlink.com/content/m762...

describing a format to record and exchange proofs.

I am already working with a couple of friends

http://web.math.unifi.it/users/maggesi/

http://math.unice.fr/~ahrens/

on a way to make theorems searchable in a convenient way; we computed pagerank on the graph of the whole standard library of Hol Light theorems, and working on how to make the best use of this ranking in search.

One of our findings is that the theorem wich uses more other thms for its proof is the existence of the GCD

http://en.wikipedia.org/wiki/Greatest_co...

and the theorem with the highest pagerank in the graph is the induction theorem over natural numbers

http://en.wikipedia.org/wiki/Induction_t...

Some scripts and data we used are hosted here:

http://ks3097767.kimsufi.com/gitweb/?p=h...

http://ks3097767.kimsufi.com/gitweb/?p=h...

A quite incomplete documentation effort is here:

http://ks3097767.kimsufi.com/gitweb/?p=h...;

Unfortunately I don't permit anonymous clone of the git repo because... (cough) I don't know how to set it up on my server (cough cough), but i'll move everithing to github very soon.

Disclaimer: this is just something we do on weekends!

Wait man, are you going to seat in your garage collecting all theorems since mathematics was born? It would take some time...

No! it's already done! Read on.

Since the invention of automated theorem provers and proof assistants,

http://en.wikipedia.org/wiki/Automated_t...

http://en.wikipedia.org/wiki/Proof_assis...

a lot of effort have been put into writing statements and proofs of theorems in a machine readable form, and there are huge libraries already availables. Nonetheless, proof assistants has been constantly improved, leading to a better understanding of mathematics. Some of the major softwares are

http://en.wikipedia.org/wiki/Coq

http://en.wikipedia.org/wiki/HOL_Light

As of today, some of the brightest matematicians in the world are working on the "formalization" of the proofs of the Kepler Conjecture

http://mathworld.wolfram.com/KeplerConje...

and the classification of the finite simple groups.

http://en.wikipedia.org/wiki/Finite_simp...

The four colors theorem was formalized in 2005

http://en.wikipedia.org/wiki/Four_color_...

We are now at the point where a field medalist like Vladimir Voevodsky

http://en.wikipedia.org/wiki/Vladimir_Vo...

opened a github repo

https://github.com/vladimirias/Foundatio...

and started hacking!

Moreover, something happened in 2006: the need of transporting theorems from a system to another led to this paper,

http://www.springerlink.com/content/m762...

describing a format to record and exchange proofs.

I am already working with a couple of friends

http://web.math.unifi.it/users/maggesi/

http://math.unice.fr/~ahrens/

on a way to make theorems searchable in a convenient way; we computed pagerank on the graph of the whole standard library of Hol Light theorems, and working on how to make the best use of this ranking in search.

One of our findings is that the theorem wich uses more other thms for its proof is the existence of the GCD

http://en.wikipedia.org/wiki/Greatest_co...

and the theorem with the highest pagerank in the graph is the induction theorem over natural numbers

http://en.wikipedia.org/wiki/Induction_t...

Some scripts and data we used are hosted here:

http://ks3097767.kimsufi.com/gitweb/?p=h...

http://ks3097767.kimsufi.com/gitweb/?p=h...

A quite incomplete documentation effort is here:

http://ks3097767.kimsufi.com/gitweb/?p=h...;

Unfortunately I don't permit anonymous clone of the git repo because... (cough) I don't know how to set it up on my server (cough cough), but i'll move everithing to github very soon.

Disclaimer: this is just something we do on weekends!

# NOTE: code repo is 1.2 MB

git clone http://ks3097767.kimsufi.com:/git/holran...

# NOTE: data repo is 73 MB

git clone http://ks3097767.kimsufi.com:/git/holran...