Another excellent point. Right now it's a "winner takes all" competition. It matters to prove a result, and much less to provide an "elegant" proof. I can only hope for a future where we measure the algorithmic entropy of a proof [log proof length][0], and results like "ABC theorem proof using half the bits as best known proof" become notable.

[0] https://en.wikipedia.org/wiki/Kolmogorov_complexity

I'm interested in your $HOBBYPROJECT. I'm hoping to develop some software similar to edukera.com, ie using proof assistants as educational tools for mathematics. Would love to swap some cool links and references. Thanks!

I'm actually in the process of (poorly) implementing my own proofs engine to try and gain a deeper appreciation for the notions behind type theory (and how eg Coq operates):

That a function is the same thing as a proof, with the theorem it proves being the type it constructs and its assumptions being the types it takes in. (Functions are proofs (which in this case, are things that take witnesses of their assumptions and produce witnesses of their theorem), values are witnesses that something is true, types are theorems, etc.)

I have an interest in topology, and want to understand HoTT, but my intuition around type theory wasn't up to par -- so I'm trying to tackle it in a constrained setting (ie, not proving theorems about mathematics as such, but a narrower problem space). Figured there was nothing to do besides get into the messy bits of it.

Can you tell me a bit more about what you're trying to do?

Hah, I'm in the same but opposite situation: I, too, am working on a Coq-like proof assistant, but I understand the type theory far more than the topology needed for HoTT.

Do you have any suggestions for simple introductions to HoTT, especially for someone without the topology background?

My background may be showing, but it may be hard to appreciate HoTT without understanding the role of homotopies in topology. My (limited) understanding of the material is that it's an attempt to introduce a homotopy structure on the type system, and then use that to talk about logical equality (mumblemumble) being the same as homotopy equivalence.

It's then using that equivalence structure between the proofs to reason about constructing proofs, as you can reason about the constructions that are possible out of classes of proofs. And that's basically where I get lost, because I don't quite know enough type theory to understand the structure they're trying to build, so I can't quite get the specific motivations. (The obvious high-level one is better formal reasoning.)

I haven't been following HoTT super closely for a year or two, getting sidetracked into the background, but last I checked there wasn't a ton of simple material on it -- it was sort of read the book, read the Coq proofs/framework, and figure it out. (Though, this easily could have changed.)

Fully agree. But person probably got flagged for commenting that what is important to hn may not be what's important to mathematicians.