4 ms·
> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer in
by munchler 2y ago
> Lean did that irritating thing which it sometimes does: it complained about the human presentation of an argument in the standard literature, and on closer inspection it turned out that the human argument left something to be desired.
Tongue-in-cheek irritation aside, this is actually awesome. I think Lean (and other theorem provers) are going to end up being important tools in math going forward.
- FredPret 2y agoCompilers have this very same habit!
- munchler 2y agoYes. In fact, Lean is a compiler and type checkers are theorem provers (by the Curry-Howard correspondence). Proofs are programs!
- dboreham 2y agoAnd Mathematics is Computer Science. Took me most of a lifetime to realize this.
- pkoird 2y agoI'd argue for the converse: Computer Science is Mathematics
- practal 2y agoLet's just say there is a really big overlap between the two. And each one can learn from the point of view of the other.
- hughesjj 2y agoThen we have the ghosts of information and category theories underpinning/influencing them all (including physics) (to some degree)
- naasking 2y ago> I'd argue for the converse: Computer Science is Mathematics The space of programs is arguably larger than the space of mathematical systems, because programs can be logically inconsistent. This suggests that mathematics is a logically consistent subset of computer science, not the other way around.
- anthk 2y agoAnd then you are wrong because everything now theorized into CS was already a thing in Math since long ago. Lisp? Knuth and computation? Lambda Calculus did it before. ] https://en.m.wikipedia.org/wiki/Lambda_calculus https://en.m.wikipedia.org/wiki/Lambda_calculus And, before computers, we had these: https://en.m.wikipedia.org/wiki/State_machine https://en.m.wikipedia.org/wiki/State_machine https://en.m.wikipedia.org/wiki/Control_theory https://en.m.wikipedia.org/wiki/Control_theory
- gedpeck 2y agoThere are statements provably true about the natural numbers that can’t be proven in first order PA. Are such statements part of computer science? If so, how?
- jerf 2y agoThat question contains so many false or unnecessary assumptions that it would take far longer to unpack them than it took you to type them, so I will limit myself to the observation that we do not even remotely confine ourselves to first order anything in computer science, nor should we.
- gedpeck 2y agoWhat false assumption did I make? I just pointed out a fact and asked a question. How many false assumptions could I have made with just one statement of fact and two questions? If you don’t have a valid answer to the question then don’t respond. I’m a mathematician and not a computer scientist. The first order PA axioms are recursively enumerable. Hence it’s clearly something of interest to computer scientists. The second order PA axioms aren’t so…are they part of computer science? What do computer scientists think about proofs in second order PA? There are no computable models of ZFC so wouldn’t it be the case that while computer scientists deal with ZFC that ZFC isn’t part of computer science? what is your definition of computer science? Physicists deal with a vast amount of mathematics but math isn’t physics. In the same way mathematics isn’t computer science. Overall I think most mathematicians would not consider mathematics as part of computer science.
- immibis 2y agowhy should computer science be limited to things that are first order PA?
- gedpeck 2y agoIt shouldn’t and I didn’t say it should. I gave a fact and asked a question. Why is PA_2 computer science? Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of computer science?
- deleted 2y ago[deleted]