Request for formalisation feedback: Algebraic Wheels

Stream: new members

[Yan Yablonovskiy 🇺🇦]

Hey all,

I am requesting feedback on the formalisation project: https://github.com/YanYablonovskiy/AlgebraicWheelTheory

NO AI OF ANY SORT HAS BEEN USED TO ANY CAPACITY IN THIS PROJECT.

All the results are currently in: https://github.com/YanYablonovskiy/AlgebraicWheelTheory/blob/master/AlgebraicWheelTheory/Basic.lean

It is very early on, but i don't want to go deep into it to discover a lot of code debt.

Specifically i would love feedback on best practices, design patterns , tips/tricks and golfing.

Any feedback is appreciated.

[A.]

(Have we got both "digitize" and "mechanize" as synonyms for "formalize" now? I don't see the need.)

[Yan Yablonovskiy 🇺🇦]

A. said:

(Have we got both "digitize" and "mechanize" as synonyms for "formalize" now? I don't see the need.)

I am too new to know for sure, I sort of decided to inherit it from https://github.com/james18lpc/GibbsMeasure/ .

@Yaël Dillies Do you recall why this word was chosen instead of mechanize?

[Yaël Dillies]

"formalise" = "write in a formal language", "digitise" = "make available to computers", "mechanise" = "render automatic ". Formalising isn't necessarily digitising (eg if you use Russell and Whitehead's formal language, on paper), and you can digitise without formalising (for example all the online libraries), but in practice formalising is a quasi-subset of digitising. Mechanising almost always involves borh digitising and formalising, and formalising gives opportunities to mechanise (by making it possible to write a new tactic, for example) but all formalising doesn't necessarily involve mechanising (you can write a proof without writing any new tactic to make it less manual).

[Philippe Duchon]

I took "mechanise" to be a synonym for "formalise" (in this context at least), because of the nature of type-theoretic proof assistants (and possibly some others as well): checking that the proof is correct is a purely mechanical (as in, computational, but computing did inherit some of its terminology from its beginnings based on mechanical devices) process.

[Yan Yablonovskiy 🇺🇦]

One reason i liked digitize a bit more when you are using a Blueprint, is that you are also transferring it into a web format with cross-referencing to the "mechanisation" (or what have you). Whereas without this, mechanize has a bit more appeal, if you are simply turning it into machine executable code without any further digital transformation or deeper annotation.