6
$\begingroup$

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)

$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$ Jul 14, 2013 at 17:35
  • 1
    $\begingroup$ 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. $\endgroup$
    – Amzoti
    Jul 14, 2013 at 17:35
  • $\begingroup$ It's not clear how this question relates to you subject - how would such a language help you learn mathematics? $\endgroup$ Jul 14, 2013 at 17:36
  • 1
    $\begingroup$ @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. $\endgroup$
    – Git Gud
    Jul 14, 2013 at 17:37
  • $\begingroup$ 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. $\endgroup$
    – user70530
    Jul 14, 2013 at 18:45

3 Answers 3

3
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ "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. $\endgroup$ Aug 15, 2015 at 11:44
2
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ The software project Prof. Gowers is talking about is about a program which can write proofs in natural language, not a proof checker which works in natural language. As far as I'm aware, there isn't such a thing as the latter (yet), but there are other proof checkers out there, such as Coq: en.wikipedia.org/wiki/Coq $\endgroup$
    – Andrew D
    Jul 14, 2013 at 18:34
1
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .