← Back to context

Comment by solomonb

3 days ago

If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev

8 comments

solomonb

Reply
hyperhello  3 days ago

If it really is formalized, it seems like the exact ideas would be able to be translated to and from any other sufficiently capable language without gaining or losing anything.

  • solomonb  3 days ago

    "sufficiently capable" is doing an insane amount of heavy lifting here. Like you can only interpret a theory into another one if the target is at least as strong as the source and even then "to and from" is a MUCH stronger condition that most pairs of theories do not satisfy.

    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.

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

  • solomonb  3 days ago

    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.

    • lioeters  2 days ago

      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

      1 reply →