Automated Theorem Proving - Mel Nathanson

By

How Harmonic's "Mathematical Superintelligence" System Aristotle 

Solved Some of My Problems

from Mel Nathanson on Research Seminars (04/30/2026): https://researchseminars.org/seminar/New_York_Number_Theory_Seminar:

Several open problems from my paper ``Problems and results on intersections of product sets and sumsets in semigroups" (arXiv:2604.04781) were recently solved by Aristotle, a formal reasoning agent developed by Harmonic. The solutions were published on April 20, 2026, in the paper ``Global product intersections sets in semigroups" by Wouter Van Doorn, Pietro Monticone, and Quanyu Tang (arxiv:2604:18869). This talk will describe product intersection sets, the open problems solved by Aristotle, what parts of the solution were in the original paper, and what exactly was the new idea that Aristotle invented to solve the problems.


Source Paper from Mel Nathanson

Problems and Results on Intersections of Product Sets and Sumsets in Semigroups

Melvyn B. Nathanson

For a family  of subsets of a semigroup, the product intersection set records those exponents  for which the -fold product set of the intersection, , is equal to , the intersection of the product sets. Nathanson recently asked which subsets of  can occur as a product intersection set, both for arbitrary and for decreasing families . We solve both problems by giving a complete classification. In particular, when , we show that in either case any subset  with  occurs as a product intersection set. Both classifications were autonomously discovered and formally verified in Lean by Aristotle, a formal reasoning agent developed by Harmonic.


Response to the Source

Global Product Intersection Sets in Semigroups

Wouter van Doorn, Pietro Monticone, Quanyu Tang
For a family  of subsets of a semigroup, the product intersection set records those exponents  for which the -fold product set of the intersection, , is equal to , the intersection of the product sets. Nathanson recently asked which subsets of  can occur as a product intersection set, both for arbitrary and for decreasing families . We solve both problems by giving a complete classification. In particular, when , we show that in either case any subset  with  occurs as a product intersection set. Both classifications were autonomously discovered and formally verified in Lean by Aristotle, a formal reasoning agent developed by Harmonic.


About Aristotle from Harmonic

On Harmonic

On Mathematical Superintelligence

Aristotle: IMO-level Automated Theorem Proving

Aristotle as a Solver

Aristotle as a Solver




Comments

Post a Comment

Popular posts from this blog

Computing and the Linguistic Turn

By
Image
Enigma (Wikipedia) Symbolic analysis and statistical analysis were both approaches codebreakers took in breaking Enigma. The development of AI has also incorporated both approaches. One historical question for AI is why the dominance of Symbolic AI from 1950 to 1990? Note the development of AI out of the Dartmouth Workshop and especially the contributions of one of its attendees,  Ray Solomonoff , to the statistical approach, an approach taken up by Marcus Hutter , a DeepMind  researcher. Note too that along with the difference between the symbolic and the statistical is the difference between language learning and computer vision. The turn Richard Sutton takes is to push learning outside the context of language, which is to push computing beyond its linguistic turn. The Linguistic Turn from Philosophy to Artificial Intelligence The Linguistic Turn   The Linguistic Turn The Linguistic Turn ,  The Linguistic Turn ~ * ~ The Bitter Lesson First Richard Sutton Richard ...
Read more

A Heidegger - Bayes Hybrid Model

By
Image
A Conjecture for a Hybrid Model Bayesian epistemology concerns modelling and specifically, belief, but a Bayesian belief does not need to be fully formed to emerge alongside the Heideggerian to-hand. The Heideggerian to-hand thereby becomes the interaction that generates this further, which is, with this interaction, a certain realization of being in the world. Bayesian selection now concerns available beliefs as well as any to-hand [belief(s)]. How Heidegger Can Make You a Better Guitarist Bayesian Philosophy Bayesian Philosophy Bayesian Epistemology Bayesian Epistemology Bayesian Modelling Bayesian Modelling Bayesian Model Selection David Deutsch on Bayesian Epistemology Bayesian Philosophy of Science Bayesian Philosophy of Science A Bayesian Approach to the Philosophy of Science On Sean Carroll on an Application of Bayes The Heideggerian To-Hand On Heidegger On Heidegger Flipping Descartes Ready-to-Hand and Present-at-Hand Presence-at-Hand Ready-to-Hand and Unready-to-Hand Does Hei...
Read more

Art and the Golden Ratio

By
Image
The Golden Ratio and Its Rectangle Dynamics ...  Harriss Spiral Harriss Spiral Harriss Spiral (Code) Harriss Spiral (Variant) The Golden Ratio  Golden Ratio Golden Ratio The Golden Ratio in Art A Critique of the Application of the Golden Ratio to Art (Keith Devlin) Making the Invisible Visible by Keith Devlin Continuation of the Critique (BeSmart) Be Smart References Counter Argument Counterargument .
Read more