3 ms·
Type theory and lean is more interesting to people who like computers than to people who like math.
by groundzeros2015 6mo ago
Type theory and lean is more interesting to people who like computers than to people who like math.
- baq 6mo agocitation needed, Tao certainly is on record using Lean and that carries some weight. also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.
- groundzeros2015 6mo agoThe link is exactly what I’m saying. I only hear cs people talk about it. For mathematicians a proof is a means to an end, or a medium of expression - they care about what they say and why. The correspondence isn’t about C programs corresponding to proofs in math papers. It’s a very a specific claim about kinds of formal systems which don’t resemble how math or programming is done.
- gowld 6mo agoMathematicians care about interesting ideas, not whether their theorems are true :-)
- groundzeros2015 6mo agoThey care about if it’s true. But the role of the formal proof is a kind of spell checker or static analysis after they have the idea.
- j16sdiz 6mo ago> They care about if it’s true. Not always. If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.
- BigTTYGothGF 6mo ago> If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true. I trust you have some examples of this?
- sincerely 6mo agoI think they're talking about conjectures that are unproven but seem "likely true" and people build further math off the assumption. E.G Reimann hypothesis
- ianhorn 6mo agoComplex numbers and Schwartz distributions (the thing the dirac delta is) come immediately to mind. “Not all numbers have square roots, but what if they did?” It seems like a common pattern.
- soulofmischief 6mo agoTerence Tao, one of the most important living mathematicians, specifically embraces Lean and has been helping the community embrace it. What you've done here is an overgeneralization. "People who like math" and "people who like computers" are massive demographics with considerable overlap.
- groundzeros2015 6mo ago> one of the most important living Maybe. But more clearly one of the most popular online.
- lanstin 6mo agoHe's a Field's Medalist so that's automatically one of the most important living. He is good at explaining things; I leaned on his Analysis textbooks when I was taking analysis and functional analysis to great effect; in a research class I was trying to calculate Fourier transforms of algebraic sets and found various almost throw away comments on his blog that were extremely enlightening (alas only to the extent I could follow them). He's a legit great mind of modern mathematics - and also able to communicate well; a historical rarity indeed. The topic being discussed here has been addressed specifically in his mastodon posts - the pre-LLM math process was understood to be "state a proof, validate a proof" - but the real aim was the not explicit "digest the proof so we can extend to other results" - with LLM/lean making the first two a lot easier and possible to do without accomplishing the digestion into the mathematical community; so we need to add "digesting proofs (from where ever)" into the job description. Thread starts here: https://mathstodon.xyz/@tao/116477351524980995 https://mathstodon.xyz/@tao/116477351524980995
- vitriol83 6mo agoFormalised proofs and Lean in particular are still too cumbersome for the ``working'' mathematician to use it day-to-day for research-level math. But clearly there is some interest on where it may take us in future.
- ux266478 6mo agoThe set theorists decided that mathematics is the overarching superdomain over all study of structure. You don't get to pick and choose. Either mathematics is a suburb of logic and these two things are separate, or they're not and ZFC dogmatics need to accept they don't have a monopoly on math. I of course fully support reinstating logicism, but the same dogmatics love putting up a fight over that as well.
- groundzeros2015 6mo agoMathematicians use logic to talk about the mathematical world. But logic is not the world.
- ux266478 6mo agoNot even the most dogmatic of the set theorists ever argued mathematics was possible without reason, however. For mathematics, logic is the world, as the copula makes no distinction between substance and existence. In the same sense that the earth is not matter itself, but it is a material thing. Putting that aside, to make things more clear: computer science is mathematics. Computer scientists are mathematicians. That was a categorization decided long before you and I ever lived. In the sense that you mean, you're only referring to a very small fraction of what "mathematics" refers to In the true sense of the word. It is just as irreconcilably disjointed as Logic is, not unified and fundamentally non-unifiable. I too think it would be better if "mathematics" was reserved for the gated suburb of ZFC. But that's not the world we live in, courtesy of the same people who pushed ZFC as a foundation to begin with.
- groundzeros2015 6mo ago> For mathematics, logic is the world, as the copula makes no distinction between substance and existence. No. There are truths about the subject not captured in any single formal system. Which is why objects are studied form many perspectives. > Computer scientists are mathematicians. Some are and some aren’t.
- smj-edison 6mo ago
- deleted 6mo ago[deleted]
- kccqzy 6mo agoI would’ve expected that people who like computers will converge around something like Idris. It’s marketed as a development tool, not a tool for formalizing mathematics even though it could be used as a proof assistant.