# Programming language to learn mathematics

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)

• Determining whether a statement has a proof is the same computation, essentially, of determining whether a program halts. Since the halting problem has no programmatic solution, neither does your proof question. Jul 14, 2013 at 17:35
• Maybe look into this list of CAS. Also, it may be worthwhile to look at Haskell, DC Proof and META-Proof as things to think about, along with Andrew's comment. Jul 14, 2013 at 17:35
• It's not clear how this question relates to you subject - how would such a language help you learn mathematics? Jul 14, 2013 at 17:36
• @Maik There's something like that, yes. It is mentioned in the book How to Prove It: A Structured Approach, by D.J. Velleman. It's called Proof Designer. I'm sure there is other such software. Jul 14, 2013 at 17:37
• It's recently come to my attention that Python has some nice built-in elementary set theory. You may have to construct your own sets and test functions, but overall I've been pleased with how intuitive programming in Python is.
– user70530
Jul 14, 2013 at 18:45

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.

• "Mathematica is not for writing proofs and doing mathematics." Mathematica may not be a proof writer but otherwise Mathematica is all about -doing- mathematics. Very much so, in fact. Aug 15, 2015 at 11:44

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.