I've started contributing recently to proofwiki (https://proofwiki.org/wiki/Main_Page) which is a similar sort of collection (this one is strictly proofs though).
I think there's a pretty big fascination among mathematicians to collect and organize the universe of information. It's always fun to think of mapping dependencies between all known proofs
Timothy Gowers wrote Is the Tricki dead? back in 2010 [1]. In it he effectively said that Mathoverflow emerged after he started it, and it seems to be better at some of the types of things the Tricki was meant for. He also talks about the fact that articles on the Tricki are harder to write, and involve more effort.
For anyone looking for a good resource for improving their mathematical problem solving (especially for the Olympiad level), I highly recommend the Art of Problem Solving wiki. [1]
That homepage isn't very informative, but you can search for any topic and find explanations and problems that can be solved from that. For example: radical axis [2]
If you're looking for a book, The Art and Craft of Problem Solving by Paul Zeitz is the most recommended.
This is interesting, but unfortunately the community looks stagnant; there have only been 5 edits and 1 new article in the last year (excluding the 2 edits I just made).
Always wanted to see something like this! Hope it'll get referenced a lot on resources like Mathworld or Wikipedia. Love the extensiveness!
Dumb question maybe, but is knowledge like this often used in symbolic solver software? If so, would it be useful to implement examples in a programming language like Gerald Sussman did in Structure and Interpretation of Classical Mechanics?
I've been working on a symbolic solver lately and have had to implement a lot of techniques manually. I'm not aware of any machine-readable database of solving techniques (which would be great for this, especially for integrals, because right now my code doesn't know any integration techniques that I don't know myself).
A lot of big solvers use algorithms[0] that can't always be reduced into a reasonable series of steps for producing nice step-by-step output, which is why e.g. Wolfram Alpha will occasionally manage to symbolically integrate something but tells you that a step-by-step solution is unavailable. (This happens even with plain algebra; Wolfram Alpha can explain how to derive the quadratic equation but not the cubic.)
Could you elaborate more on the nature of the examples from this book for those of us who haven't read it?
I always thought it would be nice to have a GitHub-like thing for formal proofs. Where anyone can define a theory using a set of axioms, and everyone else can build theorems on top of it (and on top of existing theorems), with a series of formal steps that are verified by the system.
Cameron Freer started something like this, but I think it stagnated: http://vdash.org . Tom Hales put a lot of his formal proof work on Google Code: https://code.google.com/p/flyspeck . I don't know if he has any plans to migrate to GitHub, though.
I think there's a pretty big fascination among mathematicians to collect and organize the universe of information. It's always fun to think of mapping dependencies between all known proofs