The main issue with automatic translation of mathematics into code is that mathematicians often define concepts without regard for their computability.
Here are two examples:
1. Consider the set of Turing machines that halt on a certain string. This set is logically sound, but it's impossible, in general, to create a computer program that can decide membership on the set.
2. Non-constructive "there exists" style proofs. For example, take Peano's existence theorem. This helps characterize an important class of ODEs that clearly have solutions but lends no help towards actually constructing solution(s).
Mathematicians just tend to talk about this as "constructible" instead of "computable" though. My favorite illustration of this is here: http://www.scottaaronson.com/blog/?p=103
Comments
The main issue with automatic translation of mathematics into code is that mathematicians often define concepts without regard for their computability.
Here are two examples:
1. Consider the set of Turing machines that halt on a certain string. This set is logically sound, but it's impossible, in general, to create a computer program that can decide membership on the set.
2. Non-constructive "there exists" style proofs. For example, take Peano's existence theorem. This helps characterize an important class of ODEs that clearly have solutions but lends no help towards actually constructing solution(s).
Mathematicians just tend to talk about this as "constructible" instead of "computable" though. My favorite illustration of this is here: http://www.scottaaronson.com/blog/?p=103
Interesting distinction that rings really quite true.
Interesting but recent thread on it http://news.ycombinator.com/item?id=3227620