Comment by lioeters
3 days ago
Oh how interesting, they're using a fork of Agda called Mikan, not Lean as I imagined before visiting the link. https://1lab.dev/Mikan.html
3 days ago
Oh how interesting, they're using a fork of Agda called Mikan, not Lean as I imagined before visiting the link. https://1lab.dev/Mikan.html
Yup, Mikan is a fork of Agda that focuses specifically on Cubical Type Theory. Lean's CIC is only one approach to dependent type based formal verification. Cubical gives you a computational approach to Homotopy Type Theory.
The biggest difference from Lean's CIC is how equality is handled. Lean's equality is Set like (allproofs of an equality are equal), whereas in cubical equality is higher dimensional. Equalities are paths and there can be multiple distinct paths between things. This means function extensionality and univalence are theorems that actually compute rather then be axioms or derived principles that get stuck. You also get higher inductive types "for free."
All that said I don't mention 1lab for the fact that it is Cubical. I think its a fantastic example of how to use dependent types to explore, teach, and formalize mathematics in a pro-human way.
I'd never heard of Cubical Type Theory, how interesting. Aside from that, and Mikan - why they forked, their development/contribution policy (which I happen to agree with more or less); and the notion of equality and equivalence (you didn't use this word but I read an article¹ with a glimpse into these concepts).. "Equalities are paths" - I'm going to be thinking about that for a while. Anyway the link to 1lab and the comments in this thread gave me various ideas to chew on, there's lot of substance there.
On the 1lab site, I started with simply-typed lambda calculus, an all-time classic that I've always wanted to understand more fully. How the site is designed, I love the syntax-highlighted math/code and the interface where every single concept can be clicked and hovered over to show additional information with usually a link to its own page. It led me to a kind of branching, graph-like manner of learning, where I open pages on categories, products, morphisms, uniqueness, equality - filling holes in my understanding as needed, then going back to more specific ideas built from those general foundational concepts.
An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression, to support an autodidactic and exploratory style of learning. It relates to topics raised elsewhere in this thread, like a "proper IDE for math" (integrated development environment for mathematics) and a language-agnostic "standard library" of data structures, algorithms, definitions, theorems, etc., where programming languages can import from a shared corpus of mathematically rigorous primitives.
> how to use dependent types to explore, teach, and formalize mathematics in a pro-human way
I find it meaningful how you phrased this - at this point in history with the state of technology that can overwhelm and devalue human intelligence, it's more important than ever to focus on how we teach, learn, communicate and cultivate understanding.
On a tangent, one of my interests is the book _Reflective Programs in Tree Calculus_² by Barry Jay, its proofs in Rocq, his more recent article "Typed Program Analysis without Encodings"³, and the work of his main collaborator⁴. I lack the relevant academic background to fully grasp it yet, so I've been chipping away at learning the necessary basics. So the link to 1lab is appreciated, it's a resource I'll be digging into over time.
---
¹ With Category Theory, Mathematics Escapes From Equality https://www.quantamagazine.org/with-category-theory-mathemat...
² https://github.com/barry-jay-personal/tree-calculus/blob/mas... (PDF)
³ https://github.com/barry-jay-personal/typed_tree_calculus/bl... (PDF)
⁴ https://github.com/lambada-llc/tree-calculus
What a wonderful response :)
> I'm going to be thinking about that for a while.
This is a deep and fascinating world to get into. Enjoy!
> It led me to a kind of branching, graph-like manner of learning...
Yes! I love this experience. It takes a little owrk but you can even import the 1lab as a library and re-implement whatever fragment of it you are trying to learn. Working through a proof using a proof checker is an amazing experience and is actually really fun.
The real learning (about the thing you are proving but also about type theory, programming language design, abstraction, etc) occurs while interactive with the proof checker. They all come with really sophisticated tools for interacting with the compiler and the code, interactions that are rather unlike any other ide experience.
If you wanted a place to get started I would highly recommend PLFA: https://plfa.github.io/
> An interactive textbook as a computational medium I feel has a lot more potential for usefulness and expression
I agree 100%. PLFA is a great example of something in that direction but I think we could go a lot further. I've fantasized forever about something like the illustrated primer from Neal Stephenson's The Diamond Age (https://en.wikipedia.org/wiki/The_Diamond_Age). I think that LLMs + dependently type languages could get you close to it.