If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev
Then when a translation exists the proofs can blow up in size to where you lose feasibility and understandability even tho they are technically still proofs.
Regardless of all that, I wasn't even bringing up 1lab because of the choice of language or type theory. I bring it up as an example of a pro-human way of presenting formalization.
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.
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)
> 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.
Oh I see one of the authors of PLFA is Philip Wadler, whose name I recognize from Haskell and various papers on programming language theory. There's a Lean version of the book too. https://github.com/plfa/plfl
> Working through a proof using a proof checker .. They all come with really sophisticated tools for interacting with the compiler and the code
I have some prior experience developing a specialized code editor for a template language, and remember thinking at the time how much more potential there is for an advanced interface that supports the author, that deeply integrates with type information, documentation, examples, etc. Not just for writing programs and templates, but also for "rich text" and multimedia documents - for example, including music scores, diagrams, graphs.
Speaking of dependently typed languages (whose definition I admit I don't fully grasp yet), it reminds me of a paper I find fascinating and have read multiple times.
Physics, Topology, Logic and Computation: A Rosetta Stone - https://arxiv.org/abs/0903.0340
Again I lack the foundational concepts to really understand it to satisfaction. So I'm sure the resources you recommended will be useful on my learning journey.