search into math theorems

Log in to Vote
45 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,
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

As of today, some of the brightest matematicians in the world are working on the "formalization" of the proofs of the Kepler Conjecture
and the classification of the finite simple groups.
The four colors theorem was formalized in 2005
We are now at the point where a field medalist like Vladimir Voevodsky
opened a github repo
and started hacking!

Moreover, something happened in 2006: the need of transporting theorems from a system to another led to this paper,
describing a format to record and exchange proofs.

I am already working with a couple of friends
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
and the theorem with the highest pagerank in the graph is the induction theorem over natural numbers

Some scripts and data we used are hosted here:

A quite incomplete documentation effort is here:;

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 7 months ago • type: Fathead (keyword data) Needs a Developer

now the git server supports anonymous checkout:

# NOTE: code repo is 1.2 MB
git clone
# NOTE: data repo is 73 MB
git clone
posted by [UserVoice gghh] • 6 years and 7 months ago Link
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] • 5 years and 4 months ago Link
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 6 months ago Link