2
$\begingroup$

I am looking for a math editor that is able to present equations and relations between them. I am not searching for a traditional Latex / MathML editor (I know about various online services that allow typing in equations in various formats then outputting a pretty picture). I know about online sage notebook, about mathjax and that like. I also know about Lurch and Wolfram Alpha (thanks to tp1 below).

What I'm looking for is something like pearltrees in interface with pearls being equations and edges indicating the source of the concepts (other equations or axioms). The equations should be editable and each may have an additional page that explains the equation, maybe from external source like Wikipedia.

Here is a sample tree with a direct proof directly from Wikipedia.

Consider two even integers x and y. Since they are even, they can be written as x = 2a and y = 2b respectively for integers a and b. Then the sum x + y = 2a + 2b = 2(a + b). From this it is clear x + y has 2 as a factor and therefore is even, so the sum of any two even integers is even.

(can't embed images yet)

$\endgroup$
6
  • 1
    $\begingroup$ wolfram alpha might work. $\endgroup$
    – tp1
    Apr 20 '13 at 15:31
  • $\begingroup$ thank you for the suggestion. Wolfram Alpha is a very interesting tool but this is not what I'm talking about here. What I'm talking about is ... a tree index for the content shown by Wolfram Alpha. :) What Wolfram Alpha presents is suitable for the "side pane" that would be presented when one clicks on a node. $\endgroup$
    – Nicu Tofan
    Apr 20 '13 at 15:39
  • $\begingroup$ @TNick would the result you are looking at be something that summarizes the current state of mathematics ... perhaps in a mindmap? $\endgroup$ Apr 20 '13 at 15:56
  • $\begingroup$ what I'm asking in this particular question is an user-oriented editor. Any user should be able to "import" definitions (nodes) from other users (as reference/shortcut, not importing the entire content) and build on that (similar to Lurch). So it's not about "current state of mathematics" (but that is an interesting idea on its own). Creating new content from existing content by the software is also outside the scope of this particular question (also interesting to contemplate). $\endgroup$
    – Nicu Tofan
    Apr 20 '13 at 16:14
  • $\begingroup$ okay! A small example linking basic equations to each other would help a lot when people come to read this question. $\endgroup$ Apr 20 '13 at 16:17
1
$\begingroup$

Trees for some equational proofs

Mathematica (which is Online) recently added some functionality to find proofs for some equational logic theorems and present them in various ways in both text and a tree.

There are a lot of examples/pictures at the reference page for FindEquationalProof. One particularly striking picture is a tree for a proof that one axiom implies a collection of 3 for NAND. If $(ab)$ denotes $a\,\operatorname{NAND}\,b$, then the three axioms

  1. $((aa)(ab))=a$
  2. $(a(ab))=(a(bb))$
  3. $(a(a(bc)))=(b(b(ac)))$

all follow from $(((ab)c)(a((ac)a)))=c$. Mathematica proves this in 250 steps with a tree like: proof tree for NAND logic


Trees for many theorems

This doesn't cover equational proofs yet because it's only been done for the first 1000 proofs, but Antony is working on automatically converting metamath proofs to trees at this github repository. For example, this page shows the following tree for the theorem "ccase", which roughly says that if we have $P\land R\to T$ and $Q\land R\to T$ and $P\land S\to T$ and $Q\land S\to T$, then we can derive $(P\lor Q)\land (R\lor S)\to T$: tree for ccase

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.