[HN Gopher] ProofWiki is an online compendium of mathematical pr...
       ___________________________________________________________________
        
       ProofWiki is an online compendium of mathematical proofs
        
       Author : Tomte
       Score  : 146 points
       Date   : 2022-05-07 08:50 UTC (14 hours ago)
        
 (HTM) web link (proofwiki.org)
 (TXT) w3m dump (proofwiki.org)
        
       | HidyBush wrote:
       | What's worse than mathematical proofs on Wikipedia? A whole
       | Wikipedia of mathematical proofs!
        
         | benrbray wrote:
         | 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".
        
           | layer8 wrote:
           | 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?
        
           | jacobolus wrote:
           | 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.
        
             | kragen wrote:
             | 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.
        
           | mateo1 wrote:
           | 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.
        
             | krastanov wrote:
             | I have not explored the English Wikipedia math proofs, but
             | the ones on the French Wikipedia are absolutely
             | outstanding.
        
               | mateo1 wrote:
               | It could be because they are written by a single person
               | and not edited often.
        
               | SemanticStrengh wrote:
               | 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&go
               | to=threads%... Feel free to ignore
        
       | cpp_frog wrote:
       | 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.
        
       | molly4mitchel wrote:
        
       | namibj wrote:
       | 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.
        
         | zaik wrote:
         | 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.
        
       | dwheeler wrote:
       | 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.
        
       | FabHK wrote:
       | 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 Erdos that God had a book with the
       | most beautiful proofs.
       | 
       | https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK
        
       | siraben wrote:
       | 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...
        
       ___________________________________________________________________
       (page generated 2022-05-07 23:01 UTC)