>I’ve emailed some of the mathematicians with a few proposed typo fixes, and I got confirmation that at least a few of those fixes seemed real. However, some of the problems that weren’t backed by Lean also turned out to be misunderstandings.
I think this project is really neat, but is it appropriate to cold email specialists before you've put in enough hours of effort to describe yourself as more than an "amateur"? OP's emails may have been helpful, but billions of people use these LLMs to wade into new areas and email is already low signal-to-noise.
Yeah it's a pretty tough question! I've resisted doing that until I had a relatively high certainty that their published results contained minor mistakes, which I assumed they would want to know about. I've also been explicitly apologetic and tried to keep it super brief.
A counterpoint - I was told a story by one of my professors in the late 1990s, about one of his professors -- he'd written a thesis, gotten hired somewhere like Princeton, and taught there for a few years as Dr. <Somebody>. One day he received a letter pointing out a construction flaw in his thesis. He brought it to the department head who read the letter, and said "Well, Mr. Somebody, ..." Ultimately he fixed the proof.
Upshot, if there are real errors in published work, I think most mathematicians want to know about them.
Yea but that was a person who actually put in work and had to think about and understand the problem. They didn't just generate something with a magic box.
As a software engineer, I could not care less about how a bug was found or by whom, as long as I can quickly verify it is correct, I always appreciate being able to improve my work. I don't see why it should be different for mathematicians (the ones I knew would think similarly, I would assume.)
If I may offer an analogy, what I tried to do is essentially reporting a bug after having a failing unit test that exercises the public API, without looking into the black box of internals.
> They didn't just generate something with a magic box.
It doesn't matter who found the error nor how it was found. An error is an error.
This issue really separates the wheat from the chaff. The dirty secret is that a lot of academic published work contains errors but the authors also have fragile egos. It reminds me of when Data Colada exposed someone for fraud and they accused the exposers of "methodological terrorism" (something in psychology or social science). Just imagine what happens once papers get exposed at scale.
Now here there was no fraud just genuine error, but it will annoy people nonetheless and scrape their ego that someone uninitiated can just type some stuff in a magic box and conclude that they, the established published, tenured mathematician with awards and medals can be wrong.