ProofWiki is an online compendium of mathematical proofs | Hacker News Reader

ProofWiki is an online compendium of mathematical proofs

proofwiki.org

160 pointsTomte16 comments

I remember that when I was a sophomore in high school I wanted to give a shot at higher maths and started reading some articles there. I found [0], which states that between any pair of distinct real numbers there exists a rational number. It was one of the first proofs I read, and found it so ingenious that I wrote it down and read it while commuting to school. Then I went on to study maths and found that the arguments and reasoning behind it were not that 'marvelous' [1], in fact, mathematics has several results/generalizations with the same underlying ideas (well-ordering principle, unboundedness of the naturals in this case) present as variations in any proof, not just this one. When mathematicians have a new tool we start applying it to everything we can.

Another thing, there is [2] which has not the same purpose: it covers the majority of undergrad math with lots of examples and proofs, it's more like a textbook.

[0] https://proofwiki.org/wiki/Between_two_Real_Numbers_exists_R...

[1] There is some retrospective explaining, of course, the proof was marvelous in ancient times, it's just that in the modern formal abstract setting the ground was laid to characterize number fields with the properties the ancients used.

[2] http://mathonline.wikidot.com/

EDIT: there it says the proof was featured in 2013, the same year I was a sophomore.

There's also the Archive of Formal Proofs: https://www.isa-afp.org/

It has many (all?) publicly available Isabelle (proof assistant) proofs quite neatly organized.

Explaining proofs to computers is still a very different beast to explaining proofs to humans. Hopefully this gap will get narrower in the next 50 years or so.

Here is a larger compendium of mathematical proofs that are formally proved all the way back to ZFC axioms using classical logic, namely the Metamath Proof Explorer: http://us.metamath.org/mpeuni/mmset.html

Metamath lets you state your axioms including your logic system, so there are other Metamath proof databases that make different assumptions.

If you enjoy proofs, you'll enjoy Proofs from THE BOOK, a collection of beautiful proofs. The title of the book is an allusion to the notion by Paul Erdős that God had a book with the most beautiful proofs.

https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

ProofWiki is an amazing resource for someone studying CS and math like myself. Definitions and lemmas are hyperlinked and the proof style is very clear. They even have multiple proofs for the same theorem. For instance[0], and they have a wide range of deeper topics such as measure theory[1].

Good proof style is like good program style, if you use a big hammer of a theorem (cf. library function), you risk making the result more opaque to the reader than necessary. Proof 1 of [0] can be understood by essentially following the definitions whereas proof 2 uses Orbit-Stabilizer, but the argument is still quite slick.

[0] https://proofwiki.org/wiki/Number_of_Distinct_Conjugate_Subs...

[1] https://proofwiki.org/wiki/Pointwise_Convergence_Implies_Con...

What's worse than mathematical proofs on Wikipedia? A whole Wikipedia of mathematical proofs!

Wikipedia is can actually be a great source of high-quality mathematical exposition. It is often not the best source, but I often use it as a jumping-off point for learning about advanced topics. It helps me turn "unknown-unknowns" into "known-unknowns".

Collaborative encyclopedia writing with anonymous people on the internet turned out a lot better than expected in most cases, but writing correct and coherent mathematical proofs is not one of it's areas of success.

I have not explored the English Wikipedia math proofs, but the ones on the French Wikipedia are absolutely outstanding.

It could be because they are written by a single person and not edited often.

Hi, sorry to hijack your comment but I saw in your description that you are a researcher in quantum computing. Slightly out of domain but I was wondering what you think about this cannonical quantization of gravity https://news.ycombinator.com/reply?id=31290590&goto=threads%... Feel free to ignore

The key words here are can be. Some mathematics articles are high quality, but most are somewhere between completely inadequate and blandly mediocre. If you click through all of the math-related wiki-links in even the best mathematical articles, at least half of them are going to be a disappointment. Many articles are little more than a dry definition. In general articles are missing context, history, proofs, figures, references, .... Topics that dozens of top mathematicians focused decades-long careers on, for which there are multiple hundreds-of-pages-long excellent textbooks and dozens of papers describing the historical development, have a few measly paragraphs of text and no figures. Some high-level articles contain little more than a bullet list of wiki links. Biographies of mathematicians (except for a few exceptional famous people) generally have little to no mathematical content, and do not put work in context. Mathematicians writing in English (and some older ones in German/French) get coverage but there are huge gaps in biographies of e.g. Soviet mathematicians.

The best coverage is probably of the content of typical secondary school / undergraduate math curriculum. But even then articles are often full of lists of trivia while neglecting motivation and central ideas.

The same is true for many other parts of Wikipedia though. Writing good Wikipedia articles takes a ton of work (research, organizing, writing, revising, drawing figures, building consensus with other editors, ...), and is a distributed volunteer effort, so the quality of material that does make it online is still surprisingly impressive.

If we can get those top mathematicians to license their textbooks and papers under CC0, CC-BY, or CC-BY-SA, we can incorporate their explanations and figures into Wikipedia.

One problem with mathematical articles on Wikipedia is that there’s no DAG structure to follow. You often end up running in circles trying to understand related concepts. For many mathematical definitions/objects/theorems there’s also a lack of motivation or rationale given. Why do we have that concept/theorem? How/where is it being used in practice?

I had to agree with this. While Wikipedia doesn't necessarily provide a sound information, it does provide links to different topics, which honestly I had not idea how to 'google search'

Reply on news.ycombinator.com