CIRCLE WITH A DOT

@mevenlennonbertrand
There could be engineering value in this as a starting point to porting complete proofs, though ofc that is not demonstrated until you actually do the proofs. For example, I would consider a tool that translates Rocq canonical structures hierarchies into it's type-theoretically similar Lean code _wrong_, because in Lean, you want to use typeclasses 99% of the time. I'll reserve judgement until they fill in the gaps.

@mevenlennonbertrand I am not comfortable with having that added to the TCB, so, getting back to my initial comment I would not call it "verified" given how easy it is to get wrong! Their article brings up several differences between the Lean and Rocq type theory... can they be sure they caught them all? Apply their technique to a proof development in a different language that is not classically valid. What goes wrong? What if all the definitions they choose to port are round-trippable but some of them are not true????

The answer to this rhetorical question is probably that "they wouldn't trust that" but I think the translation is subtle enough that I wouldn't put faith in it.

You live by the post you die by the post I guess

@mevenlennonbertrand I guess I don't understand their article. I can see how you'd verify that a round-trip Rocq translation is correct (ie. identical) but doesn't that say nothing about the correctness of your Lean code when linked against other Lean code?

Adding to the TCB is not that interesting to me.

@sandmouth @JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I mean... I'm serious about it. I've seen really convincing arguments from type theorists about how Lean's type theory is missing features (transitive defeq, decidable defeq, consistency with various axioms). Some of the missing features are just mistakes, but some of them are made in the interest of usability or simplicity or speed or whatnot.

Personally, I don't think has decisively shown that these things _aren't_ in conflict, so that is the sense in which I see Lean as worse and better. Idk, just my opinion.

@mevenlennonbertrand Porting a bunch of theorem statements and then saying it's "verified" is... bold

@mevenlennonbertrand I've read that article rocq-lean-import was the only interesting thing in it

@andrejbauer @johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject

> Mathlib will soon be left in the dust of history

Totally. Even on a technical level, having one dominant math library does not signal the degradation of the field. The other day I learned about [1] for automatically porting Lean definitions to Rocq. This project now gets to start with targeting a big, consistent library of formalized math, and even if the Mathlib people won't care that's still an great thing for the field!

[1] https://github.com/rocq-community/rocq-lean-import

@JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Lean is worse, but, infamously, https://en.wikipedia.org/wiki/Worse_is_better