search into math theorems

Log in to Vote
44
44 Votes • 3 Comments
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!
• posted 6 years and 1 month ago • type: Fathead (keyword data) Needs a Developer

anonymous
now the git server supports anonymous checkout:

# 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...
posted by [UserVoice gghh] • 6 years and 1 month ago Link
anonymous
I like what you've done. Oddly, or not I use math in various ways, such as a signature qualifier. If I sign something it's associated with an individual, targeted mathematical function. You can't open the message, if you don't know which is the flavor of the moment, so to speak. Usually I use a value that's based on a topological graphic. No special reason, other then I think the ones I use to me, look pretty.
posted by [UserVoice Robert] • 4 years and 10 months ago Link
anonymous
This sounds very exciting! At this point, could you give an example of how one would type a search query for a theorem? Would it involve learning the syntax of one of the prover softwares you linked to?
posted by <hidden> • 6 years and 13 days ago Link