3 ms·
Proof assistants such as Lean are inching their way into the mainstream. Ideas from topos theory, higher category theory, and homotopy theory are all running to
by Syzygies 5y ago
Proof assistants such as Lean are inching their way into the mainstream. Ideas from topos theory, higher category theory, and homotopy theory are all running together:
https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/
I'd argue that any new programming language should be designed with an awareness of the languages of formal proof. Otherwise one is barking up the wrong tree.
Samuel Eilenberg, perhaps the most influential mathematician to pass through Columbia's math department doors, was in his later years a pioneer of topos theory. Colleagues viewed this with respect and puzzlement; no one else had much of a clue what topos theory even was.
As a kid, I saw a photo of Eilenberg "working", deep in afternoon thought while reclining in his apartment, in a Time/Life book on mathematics. I thought, "What a great job!" Years later, he called to hire me. Early on the job, I was out drinking with friends after midnight, way downtown, when a fellow postdoc spotted Sammy at the bar. "What if he sees us!?" Huh, he's here too. We moved across the street to a quieter bar, then I saw him looking for a cab, and invited him to join the four of us. We were out together past dawn, and he beat me into the department that day, as chair. He was seventy.
- spekcular 5y agoWait, what? Lean doesn't used any ideas from "topos theory, higher category theory, and homotopy theory." It uses pretty vanilla type theory. The HoTT people sometimes express annoyance at the "impurity" of their approach, in fact. Also, it's not so clear that Eilenberg is "most influential mathematician to pass through Columbia's math department doors" when people like Okounkov are there. I don't necessarily disagree, but it's a highly contestable claim.
- deleted 5y ago[deleted]
- bionhoward 5y agoIt’s a good claim. Topos theory is a statement about type systems, right?
- Syzygies 5y agoLean is getting the most math buzz of late. The HoTT people instead use Coq, which has to be adapted to their purpose. The differences could be its own thread. I love how you allow that dependent types are now "vanilla"; perhaps more people will migrate from Haskell to Idris. The HoTT book is the trippiest read. I said "perhaps", and what's an opinion worth if it's not obviously an opinion? Eilenberg has category theory and homological algebra to his credit, those are entire subjects that have shaped the last seventy years of mathematics. I'm happy to throw him into the debate.
- zozbot234 5y agoAIUI, it is possible to do HoTT in Lean 3 with no modifications to Lean itself, albeit by "disabling" singleton elimination from Prop to Type. (An example library is at https://github.com/gebner/hott3 https://github.com/gebner/hott3 .) No idea about the newer Lean 4, but the documentation does not mention any changes to the underlying logic that would affect that.