Month: July 2020

Small observations on fields in Lean

~ David Roberts ~ 5 Comments

This started out at a comment on Kevin Buzzard’s recent blog post on division by zero in Lean, but I got caught up in my own thoughts, and was turning into one of those “I have a question but it’s more of a mini-talk about my own ideas” non-questions at seminars. So I moved it here.

The background is this: in the proof assistant Lean, fields are defined so that inverse is an everywhere-defined function, with the inverse of zero being zero. Kevin points out that this doesn’t actually change anything, since the axioms on fields explicitly demand that you can only get a\cdot a^{-1} = 1 if you know a \neq 0. In Lean, this means you have to supply a proof that this is the case. So one cannot abuse 0^{-1}=0 in incorrect proofs that would use actual division by zero. There is no mathematical difference between defining inversion as a total function, and only defining axioms in ‘guarded’ situations, and only defining inversion as a partial function. The fact that 0^{-1}:=0 is, from a programming point of view, fairly arbitrary; the output (i.e. the right hand side of the :=) could be any “junk” value. In other languages one might specify it to be ‘NaN', and have rules about how that interacts via addition and multiplication.

Continue reading “Small observations on fields in Lean” →

Thank you, kind referee! :-)

~ David Roberts ~ 1 Comment

Got a referee report back on a paper that took a long time to get right, but which I thought for a long time wasn’t worth even submitting for publication. My favourite remark from the report:

The proofs are clear and easy to follow, but the end results are non-trivial, and with clear applications.

There has been online discussion recently, which I have glimpsed but not followed in-depth, on who we as mathematicians write papers for. The stereotype of a genius mathematician whose papers are inscrutable to all but those on the inside circle who have access to the great man is not one that I find appealing. Yes, mathematics has prerequisites on knowledge, but it can also make sense when explained well. I am flattered that my proofs, which I struggled to write in an elementary way as possible, are seen by at least one person as clear, while also appreciating the scope of the theorem. There are of course things to fix and further clarify, and so this is refereeing at its best: seeing the worth of a paper (I am clearly no great judge of my own work), but finding ways to improve and suggest extra useful context. The scrutiny was very close, to the point of identifying an object that was written in a canonically isomorphic form, and in context, this was not correct. Had this paper been rejected from the journal, but I had gotten the same report, the blow would have been very much softened. So I repeat: thank you, kind referee!