Programming language to learn mathematics

Question

I am a computer scientist who programs since 3 years. I am currently in my 4th semester and I struggle with some math classes, not because they are extremely difficult but they are taught extremely boring and I get no feedback at all.

Because I am totally in love with programming and I program everyday I thought it must be possible to write an universal math programming language.

So that I could do something like this

Proof ( (A ∩ B) ∪ C = A ∩ (B ∪ C) ⇐⇒ C ⊆ A ) => { // do the proof }

And then it would tell me if it would be correct.

Does something like this exist?

I was looking at http://www.wolfram.com/mathematica/ but I am not sure if this is what I actually want.

Another example would be:

For example if I have to proof ForEach x element_of N; x|7; fib(x)|7. Then I could write let x = 7; fib(x) equals 13 => result (proof_is_wrong)

Answer 1

There is something like this called Coq (the website is slow sometimes, unfortunately). You can write proofs in it and check them. Another software is Isabelle. You can write a wide range of proofs in both, and there are others as well but I suggest you start with these (they keyword to search is "proof assistant").

For instance in Isabelle, their respository of proofs shows the rank-nullity theorem in linear algebra and Fermat's Last Theorem for exponents 3 and 4. A proof of the four-colour theorem (roughly, any map needs at most four colours to be coloured so that no two countries sharing a more-than-point border share the same colour) has also been implemented in Coq.

If you are familiar with programming you ought to be able to write simple proofs in it pretty soon, though the ability to write proofs by hand is also pretty important and it is unlikely that the software alone will make you good at this, though it might help ward off the boredom. Mathematica is not for writing proofs and doing mathematics, but rather for algebra and other symbolic mathematics.

Answer 2

In fact, there is something sort of along the lines of what you ask about (weakly sort-of). The Fields Medalist Timothy Gowers has been working with the computer scientist, linguist, and mathematician Mohan Ganesalingam to develop automated proof-writing software. For example, one of the things it can do it write a proof showing that the intersections of two open sets in a metric space is an open set, or that closed subsets of complete metric spaces are complete.

For more about this, I direct you to Dr Gowers' blog post about it (the two posts before and after are also about it, if your interested).

I should mention that it's the only software I've heard of that can prove non-menial things in a reasonable way. But as far as I know, there has been no attempt to try to feed it proofs to see if the proofs are correct. However, I bet it could be done in certain cases.

Answer 3

I think Mathematica is a very powerful tool, but it's a huge program, completely closed-source and with an inteface that seems much more like a shell, more than a real programming language. Anyway, it might be of great help when you don't understand a mathematical concept.

But here's why Mathematica is not for you: it is simply not, as you said, an universal math programming language. It doesn't exist because a programming language is not intended to give, for example, formal proofs about some statement you give to it.

If you're really interested in this kind of thing, you don't need to look for a language: rather check out a program: Coq, a formal proof management system.