Michael Kinyon
ProfKinyon@mathstodon.xyz
<p>Mathematics professor at the University of Denver | research: quasigroups, semigroups, automated deduction | same username on other social media</p>
Posts
-
View post
Told my wife I couldn&#39;t talk to her anymore because she had reached her daily token limit. She did not take it well.
-
View post
Inserting a comma and then removing it again on all my projects so that when my collaborators log in to Overleaf and see the &quot;Last modified&quot; column, they&#39;ll think I&#39;ve been hard at work.
-
View post
T sv tkns, rmv ll vwls frm yr prmpts
-
View post
CAUTION: This email originated from outside the University. Don&#39;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&#39;t we good enough for you? Is this how you repay us after all these years?
-
View post
My new favorite way of doing research-level mathematics is clicking the Continue button every once in a while.
-
View post
If someone tells you they are &quot;architecting&quot; something, you should be legally allowed to hit them in the face with a banana cream pie. I can&#39;t imagine this opinion being controversial.
-
View post
I asked Gemini if it's more accurate to say that LLM's are sycophantic or obsequious, and it said that was one of the best questions it had ever been asked.
-
View post
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.
-
View post
@christianp Good grief!
-
View post
I haven&#39;t had time to install Lean so in my (very few) spare moments, I&#39;ve been playing @xenaproject&#39;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&#39;t get it to work so I had to proc...
-
View post
@tao On BlueSky, Kevin ( @xenaproject ) said you were collecting proofs of &quot;650 implies 448&quot; (or really, &quot;650 implies xy=x&quot;). I found a 27 step Prover9 proof and have just finished &quot;humanizing&quot; it. I did not look at the Vampire proof, but instead started from scratch, using methodology described in [1]. I&#39;ll just email you the LaTeX&#39;ed PDF and the Prover9 proof itself. I don&#39;t speak Lean-ish so I can&#39;t do that...
-
View post
&quot;Michael, did this researcher, whose name and affiliation are printed so clearly, coauthor this paper with you?&quot; No, ResearchGate, you&#39;re dreaming, go back to sleep.
-
View post
Here is what I just put under &quot;Professional Service&quot; in my annual self-evaluation: &quot;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?&quot;
-
View post
As associate editors, it is our duty to protect the mathematical integrity of Communications in Algebra in all arenas in which our expertise applies, and it is in this aspect where our concern lies. The "top-down" management that Taylor and Francis seems to be implementing is running roughshod over the standard practices of the refereeing process in mathematics. To unilaterally implement a system that demands multiple full reviews for papers in mathematics is extremely dangerous to the...
-
View post
Ganesan&#39;s Theorem: If R is a commutative ring with exactly n &gt; 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 ha...