Guy, have you looked at http://us.metamath.org ? Look, for example, at http://us.metamath.org/mpegif/2p2e4.html. On Tue, Mar 24, 2015 at 1:38 AM, Guy Haworth <g.haworth@reading.ac.uk> wrote:
Thanks to previous responses and to Dan, Mark, Mike and Tom ... a good set of contributions.
I was asking the question because I was thinking about a database of theorems, showing
- individual theorems as a set of initial 'constraints' leading to a 'result', but also
- showing how other theorems are used to produce the new theorem.
The 'graph' of these theorems is not a hierarchy or even a lattice ... but theorem-equivalences show that it is a more general graph.
Has anyone produced this kind of database of theorems on a computer - with access-software, GUI etc?!
I guess 'Principia Mathematica' was a first demonstration, pre computer.
Somewhere well downstream, we get to '1 + 1 = 2' with the footnote "The above proposition is occasionally useful."
Thank again - Guy
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun