flt-regular

Stream: maths

[Riccardo Brasca]

Dear all,
our paper "A complete formalization of Fermat's Last Theorem for regular primes in Lean" is now online. As usual all comments/suggestions are more than welcome.

[Bhavik Mehta]

A question not a complaint - in the second paragraph you write Lean4 in smallcaps - is this the new standard way of writing it?

[Riccardo Brasca]

good point, I don't know. At least it should be the same in all the paper (we are using a \Lean command).

[Riccardo Brasca]

If you some sort of "official" convention we are happy to follow it

[Bhavik Mehta]

There's https://docs.lean-lang.org/lean4/doc/faq.html#is-it-lean-lean-or-ln, which is what I usually follow, but I don't know of any actual requirements in any direction. That is, feel free to write it as you like!