Michael Kinyon

My new favorite way of doing research-level mathematics is clicking the Continue button every once in a while.

CAUTION: This email originated from outside the University. Don't click links or open attachments unless you know the sender and know the content is safe. Also, why are you receiving emails from outside the University? Aren't we good enough for you? Is this how you repay us after all these years?

Inserting a comma and then removing it again on all my projects so that when my collaborators log in to Overleaf and see the "Last modified" column, they'll think I've been hard at work.

A mathematician uses first person plural in proofs to suggest to the reader that they are on a journey together. This is not dissimilar to Virgil guiding Dante through the Inferno.

If someone tells you they are "architecting" something, you should be legally allowed to hit them in the face with a banana cream pie. I can't imagine this opinion being controversial.

Told my wife I couldn't talk to her anymore because she had reached her daily token limit. She did not take it well.

Ganesan's Theorem: If R is a commutative ring with exactly n > 0 zero divisors, then |R| ≤ (n+1)^2.

(Conventions: R does not necessarily have a unity; 0 itself is not a zero divisor.)

Proof: Let a_0 = 0, let a_1,...,a_n be the n zero divisors, and set a := a_1. Let b ≠ 0 be such that ab = 0. For each x in R, (xa)b = 0, and thus xa = a_i for some i = 0,...,n. For each i, let A_i = {x | xa=a_i }.

Now suppose |R| ≥ (n+1)^2+1 = n(n+1)+(n+2). By the pigeonhole principle, some A_i has at least n+2 elements, say, r_1,...,r_{n+2}. Then the n+1 elements r_1-r_2,...,r_1-r_{n+1} are nonzero and distinct, and satisfy a(r_1-r_i)=0 for each i. This contradicts the assumption that there are exactly n zero divisors. Therefore |R|≤(n+1)^2. QED

This is not Ganesan's proof, which, although easy, is not as elementary.

Commutativity isn't important; the proof actually shows that a not necessarily commutative ring R with exactly n>0 *left* zero divisors has order no more than (n+1)^2.

I can't take 100% credit for the proof. The basic idea for n=1 and n=2 appeared in a Quora answer by computer scientist David Ash in response to a question asking if there are noncommutative rings with unity with exactly two zero divisors. (Answer: no, because there are no noncommutative unital rings of order less than 8.) I noticed the connection of Ash's argument to Ganesan's Theorem and went from there.

T sv tkns, rmv ll vwls frm yr prmpts

Here is what I just put under "Professional Service" in my annual self-evaluation:

"I wrote about a dozen referee reports last year for various journals. I stopped keeping careful records of these because what is even the point?"

"Michael, did this researcher, whose name and affiliation are printed so clearly, coauthor this paper with you?"

No, ResearchGate, you're dreaming, go back to sleep.

@tao@mathstodon.xyz On BlueSky, Kevin ( @xenaproject@mathstodon.xyz ) said you were collecting proofs of "650 implies 448" (or really, "650 implies xy=x"). I found a 27 step Prover9 proof and have just finished "humanizing" it. I did not look at the Vampire proof, but instead started from scratch, using methodology described in [1]. I'll just email you the LaTeX'ed PDF and the Prover9 proof itself. I don't speak Lean-ish so I can't do that conversion for you, but if someone wants to take it on, it's fine with me.

[1] M. Kinyon, Proof simplification and automated theorem proving, Philos. Trans. Roy. Soc. A, 377 (2019), no. 2140, 20180034, 9 pp.

arXiv version: https://arxiv.org/abs/1808.04251

I haven't had time to install Lean so in my (very few) spare moments, I've been playing @xenaproject@mathstodon.xyz's Natural Number Game. At first I unknowingly played the Lean3 version. As someone who has been using automated deduction tools for two decades, I found some of it very confusing and unnatural. There were several times I had a relevant lemma and a hypothesis and all I wanted to do was a good old fashioned modus ponens, but I couldn't get it to work so I had to proceed in a roundabout way.

Then I found the Lean4 version, https://adam.math.hhu.de/#/g/hhu-adam/NNG4 , still under development. Maybe struggling with the older version primed my subconscious, or maybe it's the newly rewritten instructions, but now it all makes much more sense to me.

Having handled Peano arithmetic, I am clearly ready to fit my elementary proof of Fermat's Last Theorem into the margin of my text editor.