Professor Terence Tao analyzes how Erdős Problem 1026 was solved "through an interesting combination of existing literature, online collaboration, and AI tools." The conjecture was first proven in Lean using @HarmonicMath's Aristotle. Further patterns discovered via Show more

Yeah, proving Erdős problems with @HarmonicMath Aristotle is great, but have you tried using it to verify LeetCode-style solutions? We have. It works (invariant inference is... not fast yet). Show more

Aristotle by @Harmonic is acing group-theory puzzles. Here is a complete formal proof of the popular Yu Tsumura 554 puzzle. What's nice is that the proof is very transparent, with easy-to-follow steps. It was generated in less than an hour without any hints. I am attaching the Show more

Milestone reached: we have finished formalizing Section 3 of the Noperthedron paper! Reuben Steenekamp's work on github.com/badly-drawn-wi… gave us a significant boost, and @HarmonicMath's Aristotle has been repeatedly helpful for filling in proofs. Show more

Mathematical papers need formal validation. This is usually done informally by a referee. But what if we could rely on something more robust like auto-formalization into Lean 4 where the role of the referee would be reduced to meticulous checking of the formulations of the Show more

I used @HarmonicMath's Aristotle to formalize Erdős problem #426 in Lean 4… and ended up fully verifying a stronger bound that the original paper only suggested 🧵 Erdős offered $25 for a disproof, and $100 if the conjecture was true 👇 Show more

1/8 CompPoly is a library of machine-checked mathematics for concrete polynomial computation over rings and finite fields—the algebra behind modern cryptographic proof systems. @HarmonicMath Aristotle has recently made significant contributions to help close Phase 1 of the Show more

Meanwhile, with further prompting, ChatGPT was also able to adapt the argument to handle large 𝐶 as well as small 𝐶, thus finally producing a new result in the spirit of the intended question drive.google.com/file/d/1xRw8_… . Interestingly, the proof contained some minor errors in it, but the AI tool Aristotle was able to automatically repair these gaps and produce a Lean-verified proof.

At this point, a third particiant ran Aristotle again on the existing Lean proof to provide a shorter version, which a different participant then input into a lengthy back-and-forth ChatGPT session chatgpt.com/share/695e7cbd-605… to turn it into a much more fully fleshed article that described not just the proof itself, but its connection with prior literature and with a tighter narrative structure. This resulted in a new writeup of the proof drive.google.com/file/d/1MRQfc… that had less of the feel of a generic AI-produced document, and which I judge to be at a level of writing within ballpark of an acceptable standard for a research paper, although there is still room for further improvement. (I review this text at erdosproblems.com/forum/thread… ). (4/5)