>> Given any positive integers r and k, there is some number N such that if the integers {1, 2, ..., N} are colored, each with one of r different colors, then there are at least k integers in arithmetic progression whose elements are of the same color.
> The majority of the semantics of this statement are part of the prose.
The semantics can be expressed as prose if you like. They can also be expressed formally. As you know, 'color' is used here for the convenience of the reader. The underlying semantics works independently of the English notion of 'color'. You know this. What do you think is not formalizable about your example? "Given / assume": no problem. Introducing variables: no problem. Specifying variable types: no problem. Various mathematical structures (sets, sequences): no problem. "there are / there exits": no problem. "at least": no problem. And so on.
> Even having perfect "semantic" information about the formulas gets you absolutely nothing.
You have shared some good counterarguments, and I appreciate it, but "nothing" is an exaggeration here. It doesn't advance your argument.
> You cannot reason about this without being able to reason about human language in general like a human can
This is incorrect. You sound knowledgeable about mathematics, so I'm quite surprised you would make such a claim. Are your emotions (perhaps a loathing of Semantic MathML? -- your comments suggest this story) clouding your logic here? Deductive reasoning is well studied in computer science. To state a previous point again: there are many formal systems that can be reasoned over to various degrees. Such systems are still useful and quite different than English.
> The majority of the semantics of this statement are part of the prose.
The semantics can be expressed as prose if you like. They can also be expressed formally. As you know, 'color' is used here for the convenience of the reader. The underlying semantics works independently of the English notion of 'color'. You know this. What do you think is not formalizable about your example? "Given / assume": no problem. Introducing variables: no problem. Specifying variable types: no problem. Various mathematical structures (sets, sequences): no problem. "there are / there exits": no problem. "at least": no problem. And so on.
> Even having perfect "semantic" information about the formulas gets you absolutely nothing.
You have shared some good counterarguments, and I appreciate it, but "nothing" is an exaggeration here. It doesn't advance your argument.
> You cannot reason about this without being able to reason about human language in general like a human can
This is incorrect. You sound knowledgeable about mathematics, so I'm quite surprised you would make such a claim. Are your emotions (perhaps a loathing of Semantic MathML? -- your comments suggest this story) clouding your logic here? Deductive reasoning is well studied in computer science. To state a previous point again: there are many formal systems that can be reasoned over to various degrees. Such systems are still useful and quite different than English.