Hacker News Reader

I am wondering how much this "prove isomorphism to Mathlib equivalent" is relevant. By this I mean, would anything change if the isomorphism part would be left out, i.e. is it actually used anywhere, for example for automatically translating theorems?

View on HN

If nothing else it has pedagogical value, convincing yourself that the set and operations you established are the “same” as the ones you’re using for the rest of the book.

I loved that from the pedagogical perspective personally. When I dreamed about this textbook getting formalized, I was worried about how unwieldy the formalization could become if it strayed too far from Mathlib — but also was worried about losing the self-contained-ness if it just used Mathlib. This is a nice compromise imo.

I think that isomorphisms like this serve to establish

1. The development that you just did is equivalent to the corresponding object in Mathlib. Frequently, what is developed comes from concrete building blocks, whereas the corresponding definition in Mathlib might be a specialization of a complicated general class.

2. The basic notation and nomenclature for the object in Mathlib, which may differ.

Reply on news.ycombinator.com