https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/ [cropped-co] What's new Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao * Home * About * Career advice * On writing * Books * Applets * Mastodon+ * Subscribe to feed A proof of concept tool to verify estimates 1 May, 2025 in math.AP, math.CA | Tags: Software | by Terence Tao This post was inspired by some recent discussions with Bjoern Bringmann. Symbolic math software packages are highly developed for many mathematical tasks in areas such as algebra, calculus, and numerical analysis. However, to my knowledge we do not have similarly sophisticated tools for verifying asymptotic estimates - inequalities that are supposed to hold for arbitrarily large parameters, with constant losses. Particularly important are functional estimates, where the parameters involve an unknown function or sequence (living in some suitable function space, such as an {L^p} space); but for this discussion I will focus on the simpler situation of asymptotic estimates involving a finite number of positive real numbers, combined using arithmetic operations such as addition, multiplication, division, exponentiation, and minimum and maximum (but no subtraction). A typical inequality here might be the weak arithmetic mean-geometric mean inequality \displaystyle (abc)^{1/3} \lesssim a+b+c \ \ \ \ \ (1) where {a,b,c} are arbitrary positive real numbers, and the {\lesssim} here indicates that we are willing to lose an unspecified (multiplicative) constant in the estimates. I have wished in the past (e.g., in this MathOverflow answer) for a tool that could automatically determine whether such an estimate was true or not (and provide a proof if true, or an asymptotic counterexample if false). In principle, simple inequalities of this form could be automatically resolved by brute force case splitting. For instance, with (1), one first observes that {a+b+c} is comparable to {\max(a,b,c)} up to constants, so it suffices to determine if \displaystyle (abc)^{1/3} \lesssim \max(a,b,c). \ \ \ \ \ (2) Next, to resolve the maximum, one can divide into three cases: {a \ gtrsim b,c}; {b \gtrsim a,c}; and {c \gtrsim a,b}. Suppose for instance that {a \gtrsim b,c}. Then the estimate to prove simplifies to \displaystyle (abc)^{1/3} \lesssim a, and this is (after taking logarithms) a positive linear combination of the hypotheses {a \gtrsim b}, {a \gtrsim c}. The task of determining such a linear combination is a standard linear programming task, for which many computer software packages exist. Any single such inequality is not too difficult to resolve by hand, but there are applications in which one needs to check a large number of such inequalities, or split into a large number of cases. I will take an example at random from an old paper of mine (adapted from the equation after (51), and ignoring some epsilon terms for simplicity): I wanted to establish the estimate \displaystyle \frac{\langle N_2 \rangle^{1/2}}{\langle N_1 \rangle^{1 /4} L_1^{1/2} L_2^{1/2} } L_{\min}^{1/2} N^{-1} (N_1 N_2 N_3)^{1/2} \ lesssim 1 \ \ \ \ \ (3) for any {N_1,N_2,N_3,L_1,L_2,L_3 > 0} obeying the constraints \displaystyle N_{\max} \sim N_{\mathrm{med}} \sim N; \quad L_{\max} \ sim L_{\mathrm{med}} \gtrsim N_1 N_2 N_3 where {N_{\max}}, {N_{\mathrm{med}}}, and {N_{\min}} are the maximum, median, and minimum of {N_1, N_2, N_3} respectively, and similarly for {L_{\max}}, {L_{\mathrm{med}}}, and {L_{\min}}, and {\langle N \ rangle := (1+N^2)^{1/2}}. This particular bound could be dispatched in three or four lines from some simpler inequalities; but it took some time to come up with those inequalities, and I had to do a dozen further inequalities of this type. This is a task that seems extremely ripe for automation, particularly with modern technology. Recently, I have been doing a lot more coding (in Python, mostly) than in the past, aided by the remarkable facility of large language models to generate initial code samples for many different tasks, or to autocomplete partially written code. For the most part, I have restricted myself to fairly simple coding tasks, such as computing and then plotting some mildly complicated mathematical functions, or doing some rudimentary data analysis on some dataset. But I decided to give myself the more challenging task of coding a verifier that could handle inequalities of the above form. After about four hours of coding, with frequent assistance from an LLM, I was able to produce a proof of concept tool for this, which can be found at this Github repository. For instance, to verify (1), the relevant Python code is a = Variable("a") b = Variable("b") c = Variable("c") assumptions = Assumptions() assumptions.can_bound((a * b * c) ** (1 / 3), max(a, b, c)) and the (somewhat verbose) output verifying the inequality is Checking if we can bound (((a * b) * c) ** 0.3333333333333333) by max(a, b, c) from the given axioms. We will split into the following cases: [[b <~ a, c <~ a], [a <~ b, c <~ b], [a <~ c, b <~ c]] Trying case: ([b <~ a, c <~ a],) Simplify to proving (((a ** 0.6666666666666667) * (b ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1. Bound was proven true by multiplying the following hypotheses : b <~ a raised to power 0.33333333 c <~ a raised to power 0.33333333 Trying case: ([a <~ b, c <~ b],) Simplify to proving (((b ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1. Bound was proven true by multiplying the following hypotheses : a <~ b raised to power 0.33333333 c <~ b raised to power 0.33333333 Trying case: ([a <~ c, b <~ c],) Simplify to proving (((c ** 0.6666666666666667) * (a ** -0.3333333 333333333)) * (b ** -0.3333333333333333)) >= 1. Bound was proven true by multiplying the following hypotheses : a <~ c raised to power 0.33333333 b <~ c raised to power 0.33333333 Bound was proven true in all cases! This is of course an extremely inelegant proof, but elegance is not the point here; rather, that it is automated. (See also this recent article of Heather Macbeth for how proof writing styles change in the presence of automated tools, such as formal proof assistants.) The code is close to also being able to handle more complicated estimates such as (3); right now I have not written code to properly handle hypotheses such as {N_{\max} \sim N_{\mathrm{med}} \sim N} that involve complex expressions such as {N_{\max} = \max (N_1,N_2,N_3)}, as opposed to hypotheses that only involve atomic variables such as {N_1}, {N_2, N_3}, but I can at least handle such complex expressions in the left and right-hand sides of the estimate I am trying to verify. In any event, the code, being a mixture of LLM-generated code and my own rudimentary Python skills, is hardly an exemplar of efficient or elegant coding, and I am sure that there are many expert programmers who could do a much better job. But I think this is proof of concept that a more sophisticated tool of this form could be quite readily created to do more advanced tasks. One such example task was the one I gave in the above MathOverflow question, namely being able to automatically verify a claim such as \displaystyle \sum_{d=0}^\infty \frac{2d+1}{2h^2 (1 + \frac{d(d+1)}{h ^2}) (1 + \frac{d(d+1)}{h^2m^2})^2} \lesssim 1 + \log(m^2) for all {h,m > 0}. Another task would be to automatically verify the ability to estimate some multilinear expression of various functions, in terms of norms of such functions in standard spaces such as Sobolev spaces; this is a task that is particularly prevalent in PDE and harmonic analysis (and can frankly get somewhat tedious to do by hand). As speculated in that MO post, one could eventually hope to also utilize AI to assist in the verification process, for instance by suggesting possible splittings of the various sums or integrals involved, but that would be a long-term objective. This sort of software development would likely best be performed as a collaborative project, involving both mathematicians and expert programmers. I would be interested to receive advice on how best to proceed with such a project (for instance, would it make sense to incorporate such a tool into an existing platform such as SageMATH), and what features for a general estimate verifier would be most desirable for mathematicians. One thing on my wishlist is the ability to give a tool an expression to estimate (such as a multilinear integral of some unknown functions), as well as a fixed set of tools to bound that integral (e.g., splitting the integral into pieces, integrating by parts, using the Holder and Sobolev inequalities, etc.), and have the computer do its best to optimize the bound it can produce with those tools (complete with some independently verifiable proof certificate for its output). One could also imagine such tools having the option to output their proof certificates in a formal proof assistant language such as Lean. But perhaps there are other useful features that readers may wish to propose. Share this: * Click to print (Opens in new window) Print * Click to email a link to a friend (Opens in new window) Email * More * * Click to share on X (Opens in new window) X * Click to share on Facebook (Opens in new window) Facebook * Click to share on Reddit (Opens in new window) Reddit * Click to share on Pinterest (Opens in new window) Pinterest * Like Loading... Recent Comments [80e] nunosempere2 on A proof of concept tool to ver... [5d6] Dave Doty on A proof of concept tool to ver... [8e5] Andrew Krause on A proof of concept tool to ver... [d7f] Terence Tao on The equational theories projec... [d7f] Terence Tao on A proof of concept tool to ver... [d7f] Terence Tao on A proof of concept tool to ver... [d7f] Terence Tao on A proof of concept tool to ver... [317] Evan Conway on A proof of concept tool to ver... [d7f] Terence Tao on A proof of concept tool to ver... [d7f] Terence Tao on A proof of concept tool to ver... [9f6] Guanyuming He on A proof of concept tool to ver... [789] - on A proof of concept tool to ver... [] Anonymous on A proof of concept tool to ver... [] Anonymous on A proof of concept tool to ver... [pic] Lawrence Paulson on A proof of concept tool to ver... [ ] [Search] Top Posts * A proof of concept tool to verify estimates * Career advice * Cosmic Distance Ladder videos with Grant Sanderson (3blue1brown): commentary and corrections * Does one have to be a genius to do maths? * Stonean spaces, projective objects, the Riesz representation theorem, and (possibly) condensed mathematics * The equational theories project: a brief tour * Books * There's more to mathematics than rigour and proofs * On writing * Work hard Archives * May 2025 (1) * April 2025 (2) * March 2025 (1) * February 2025 (3) * January 2025 (1) * December 2024 (3) * November 2024 (4) * October 2024 (1) * September 2024 (4) * August 2024 (3) * July 2024 (3) * June 2024 (1) * May 2024 (1) * April 2024 (5) * March 2024 (1) * December 2023 (2) * November 2023 (2) * October 2023 (1) * September 2023 (3) * August 2023 (3) * June 2023 (8) * May 2023 (1) * April 2023 (1) * March 2023 (2) * February 2023 (1) * January 2023 (2) * December 2022 (3) * November 2022 (3) * October 2022 (3) * September 2022 (1) * July 2022 (3) * June 2022 (1) * May 2022 (2) * April 2022 (2) * March 2022 (5) * February 2022 (3) * January 2022 (1) * December 2021 (2) * November 2021 (2) * October 2021 (1) * September 2021 (2) * August 2021 (1) * July 2021 (3) * June 2021 (1) * May 2021 (2) * February 2021 (6) * January 2021 (2) * December 2020 (4) * November 2020 (2) * October 2020 (4) * September 2020 (5) * August 2020 (2) * July 2020 (2) * June 2020 (1) * May 2020 (2) * April 2020 (3) * March 2020 (9) * February 2020 (1) * January 2020 (3) * December 2019 (4) * November 2019 (2) * September 2019 (2) * August 2019 (3) * July 2019 (2) * June 2019 (4) * May 2019 (6) * April 2019 (4) * March 2019 (2) * February 2019 (5) * January 2019 (1) * December 2018 (6) * November 2018 (2) * October 2018 (2) * September 2018 (5) * August 2018 (3) * July 2018 (3) * June 2018 (1) * May 2018 (4) * April 2018 (4) * March 2018 (5) * February 2018 (4) * January 2018 (5) * December 2017 (5) * November 2017 (3) * October 2017 (4) * September 2017 (4) * August 2017 (5) * July 2017 (5) * June 2017 (1) * May 2017 (3) * April 2017 (2) * March 2017 (3) * February 2017 (1) * January 2017 (2) * December 2016 (2) * November 2016 (2) * October 2016 (5) * September 2016 (4) * August 2016 (4) * July 2016 (1) * June 2016 (3) * May 2016 (5) * April 2016 (2) * March 2016 (6) * February 2016 (2) * January 2016 (1) * December 2015 (4) * November 2015 (6) * October 2015 (5) * September 2015 (5) * August 2015 (4) * July 2015 (7) * June 2015 (1) * May 2015 (5) * April 2015 (4) * March 2015 (3) * February 2015 (4) * January 2015 (4) * December 2014 (6) * November 2014 (5) * October 2014 (4) * September 2014 (3) * August 2014 (4) * July 2014 (5) * June 2014 (5) * May 2014 (5) * April 2014 (2) * March 2014 (4) * February 2014 (5) * January 2014 (4) * December 2013 (4) * November 2013 (5) * October 2013 (4) * September 2013 (5) * August 2013 (1) * July 2013 (7) * June 2013 (12) * May 2013 (4) * April 2013 (2) * March 2013 (2) * February 2013 (6) * January 2013 (1) * December 2012 (4) * November 2012 (7) * October 2012 (6) * September 2012 (4) * August 2012 (3) * July 2012 (4) * June 2012 (3) * May 2012 (3) * April 2012 (4) * March 2012 (5) * February 2012 (5) * January 2012 (4) * December 2011 (8) * November 2011 (8) * October 2011 (7) * September 2011 (6) * August 2011 (8) * July 2011 (9) * June 2011 (8) * May 2011 (11) * April 2011 (3) * March 2011 (10) * February 2011 (3) * January 2011 (5) * December 2010 (5) * November 2010 (6) * October 2010 (9) * September 2010 (9) * August 2010 (3) * July 2010 (4) * June 2010 (8) * May 2010 (8) * April 2010 (8) * March 2010 (8) * February 2010 (10) * January 2010 (12) * December 2009 (11) * November 2009 (8) * October 2009 (15) * September 2009 (6) * August 2009 (13) * July 2009 (10) * June 2009 (11) * May 2009 (9) * April 2009 (11) * March 2009 (14) * February 2009 (13) * January 2009 (18) * December 2008 (8) * November 2008 (9) * October 2008 (10) * September 2008 (5) * August 2008 (6) * July 2008 (7) * June 2008 (8) * May 2008 (11) * April 2008 (12) * March 2008 (12) * February 2008 (13) * January 2008 (17) * December 2007 (10) * November 2007 (9) * October 2007 (9) * September 2007 (7) * August 2007 (9) * July 2007 (9) * June 2007 (6) * May 2007 (10) * April 2007 (11) * March 2007 (9) * February 2007 (4) Categories * expository (316) + tricks (13) * guest blog (10) * Mathematics (887) + math.AC (8) + math.AG (42) + math.AP (115) + math.AT (17) + math.CA (190) + math.CO (197) + math.CT (9) + math.CV (37) + math.DG (37) + math.DS (89) + math.FA (24) + math.GM (14) + math.GN (21) + math.GR (88) + math.GT (17) + math.HO (13) + math.IT (13) + math.LO (53) + math.MG (47) + math.MP (31) + math.NA (24) + math.NT (199) + math.OA (22) + math.PR (109) + math.QA (6) + math.RA (47) + math.RT (21) + math.SG (4) + math.SP (48) + math.ST (11) * non-technical (195) + admin (46) + advertising (66) + diversions (7) + media (14) o journals (3) + obituary (15) * opinion (36) * paper (253) + book (20) + Companion (13) + update (23) * question (127) + polymath (86) * talk (69) + DLS (20) * teaching (189) + 245A - Real analysis (11) + 245B - Real analysis (22) + 245C - Real analysis (6) + 246A - complex analysis (11) + 246B - complex analysis (5) + 246C - complex analysis (5) + 247B - Classical Fourier Analysis (5) + 254A - analytic prime number theory (19) + 254A - ergodic theory (18) + 254A - Hilbert's fifth problem (12) + 254A - Incompressible fluid equations (5) + 254A - random matrices (14) + 254B - expansion in groups (8) + 254B - Higher order Fourier analysis (9) + 255B - incompressible Euler equations (2) + 275A - probability theory (6) + 285G - poincare conjecture (20) + Logic reading seminar (8) * The sciences (1) * travel (26) additive combinatorics approximate groups arithmetic progressions Ben Green Cauchy-Schwarz Cayley graphs central limit theorem Chowla conjecture compressed sensing correspondence principle distributions divisor function eigenvalues Elias Stein Emmanuel Breuillard entropy equidistribution ergodic theory Euler equations exponential sums finite fields Fourier transform Freiman's theorem Gowers uniformity norm Gowers uniformity norms graph theory Gromov's theorem GUE Hilbert's fifth problem incompressible Euler equations inverse conjecture Joni Teravainen Kaisa Matomaki Kakeya conjecture Lie algebras Lie groups Liouville function Littlewood-Offord problem Maksym Radziwill Mobius function multiplicative functions Navier-Stokes equations nilpotent groups nilsequences nonstandard analysis parity problem Paul Erdos politics polymath1 polymath8 Polymath15 polynomial method polynomials prime gaps prime numbers prime number theorem random matrices randomness Ratner's theorem regularity lemma Ricci flow Riemann zeta function Schrodinger equation Shannon entropy sieve theory structure Szemeredi's theorem Tamar Ziegler tiling UCLA ultrafilters universality Van Vu wave maps Yitang Zhang RSS The Polymath Blog * Polymath projects 2021 * A sort of Polymath on a famous MathOverflow problem * Ten Years of Polymath * Updates and Pictures * Polymath proposal: finding simpler unit distance graphs of chromatic number 5 * A new polymath proposal (related to the Riemann Hypothesis) over Tao's blog * Spontaneous Polymath 14 - A success! * Polymath 13 - a success! * Non-transitive Dice over Gowers's Blog * Rota's Basis Conjecture: Polymath 12, post 3 21 comments Comments feed for this article 1 May, 2025 at 8:19 pm danielstone010 [171] Estimators and ancillary equations... I really do love this stuff. Reply 1 May, 2025 at 8:37 pm hideoutleftca8790a9b5 [474] Subject: Suggestions for Advancing Your Asymptotic Estimate Verifier Dear Professor Tao, Thank you for sharing your insightful post and proof-of-concept tool for verifying asymptotic estimates. Your vision for automating this tedious yet critical task in mathematical analysis is inspiring, and your prototype demonstrates exciting potential. As someone deeply interested in computational mathematics, I'd like to offer some constructive suggestions for developing this project further, addressing your questions about collaboration, platform integration, and desirable features. Collaboration Structure To realize a robust verifier, a collaborative team combining mathematicians, programmers, and computational experts would be ideal. I suggest: * Team Composition: Include analysis experts (e.g., in PDEs or harmonic analysis) to define inequality types and test cases, software engineers proficient in Python and optimization (e.g., linear programming with CVXPY), and specialists in computer algebra systems (e.g., SageMath) or formal verification (e.g., Lean). AI experts could enhance heuristic suggestion features. * Workflow: Adopt an agile development model with sprints focused on specific features (e.g., handling sums, functional estimates). Regular virtual workshops could align mathematical requirements with technical constraints. * Community Engagement: Host the project on GitHub to encourage open-source contributions. Outreach via MathOverflow, X, or conferences like AMS meetings could attract contributors. A hackathon to tackle specific challenges (e.g., sum verification) could accelerate progress. Platform Integration Integrating with SageMath seems a natural fit, given its open-source nature, Python-based ecosystem, and support for symbolic computation via SymPy and numerical tools via NumPy. SageMath's active mathematical community would facilitate adoption and contributions. Key steps include: * Refactoring your prototype to leverage SageMath's symbolic manipulation for complex expressions (e.g., N_{\max} = \max(N_1, N_2, N_3)). * Adding a SageMath package for your verifier, with tutorials to ease onboarding for mathematicians. * Optionally, integrate a Lean backend to output formal proof certificates, leveraging mathlib's real analysis capabilities. This could appeal to users seeking rigorous verification. While Mathematica offers powerful symbolic tools, its proprietary nature may limit collaboration. SymPy alone could suffice for a lightweight standalone tool but lacks SageMath's comprehensive ecosystem. Desirable Features Based on your wishlist and the needs of the analysis community, I propose the following features for a general estimate verifier: 1. Intuitive Input: Support LaTeX-like input for inequalities, sums, and integrals via a GUI or Jupyter notebook interface. Allow users to define constraints (e.g., N_{\max} \sim N) and function spaces (e.g., L^p). 2. Tool Specification: Enable users to specify allowed bounding techniques (e.g., Holder's inequality, AM-GM) from a library of standard inequalities, extensible with custom rules. 3. Optimization: Automatically minimize constants in \lesssim bounds using linear programming or numerical optimization. AI-driven suggestions for case splits or bounding strategies could enhance efficiency. 4. Proof Output: Generate human-readable LaTeX proofs and machine-checkable certificates in Lean or Coq. A high-level proof summary alongside detailed steps would balance readability and rigor. 5. Complex Expressions: Handle sums (e.g., your MathOverflow example) via asymptotic approximations or numerical bounds, and support functional estimates with a database of inequalities (e.g., Sobolev's). 6. Counterexamples: For false inequalities, provide asymptotic regimes where the bound fails, validated numerically or symbolically. 7. Visualization: Offer plots of asymptotic behaviors or proof trees to aid intuition. Development Roadmap A phased approach could structure development: * Phase 1 (6-12 months): Enhance your prototype to handle complex constraints (e.g., N_{\max} \sim N), add a basic GUI, and integrate with SageMath. Implement a library of common inequalities. * Phase 2 (12-24 months): Support sums and functional estimates using asymptotic methods and AI-suggested strategies. Add numerical validation for robustness. * Phase 3 (24+ months): Implement Lean proof output and optimize bounds. Release as a polished SageMath package with extensive documentation. Specific Suggestions for Your Examples * Arithmetic Inequality (abc)^{1/3} \ lesssim a + b + c: Your case-splitting approach is robust. Adding AM-GM as an alternative proof path could yield tighter constants and demonstrate the tool's flexibility. * Complex Estimate (Equation 3): Extend parsing to handle N_{\max} and \sim by defining approximate equalities as bounded ratios (e.g., c_1 N \leq N_{\max} \leq c_2 N). Numerical tests in representative cases could guide case splitting. * Sum Estimate: For the infinite sum, automate integral approximations (e.g., via Laplace's method) and regime splitting (e.g., small h, large m). SageMath's sum function could validate bounds numerically. Final Thoughts Your prototype is a compelling proof of concept, and with collaborative development, it could become a transformative tool for mathematicians. SageMath integration, a user-friendly interface, and formal proof output would maximize impact. I'd be thrilled to contribute ideas, test cases, or even code snippets to explore specific features (e.g., sum verification). Please feel free to share updates or specific challenges--I'd love to stay engaged with this exciting project! Best regards, [Going forward, I am requiring that AI-generated text be explicitly labeled as such in order to be approved as a comment. -T.] Reply 1 May, 2025 at 8:43 pm Lars Ericson [fd9] You may be interested in the work of the Exact Computation Group of Chee Yap which uses tools like Sturm Sequences, Grobner Bases and numbers represented as solutions of polynomial systems to give exact answers to inequalities on expressions involving real algebraic numbers. See Click to access isItZero.pdf leading to https://cs.nyu.edu/~exact/papers/ Get Outlook for Androidhttps://aka.ms/AAb9ysg --------------------------------------------------------------------- Reply 2 May, 2025 at 1:40 am Anonymous [] Isn't proving general inequalities (even a single one inequality) related to the theory of reals? Wouldn't the complexity issues there affect? Reply 2 May, 2025 at 5:21 am Terence Tao [d7f] Note here that I am not interested in exact (infinite precision) inequalities, but rather in estimates - inequalities "up to constants". This is a somewhat different language from the language of the reals, and in fact closer to tropical arithmetic. (Indeed, for this toy problem, one could conceivably actually phrase everything inside a tropical ring, and appeal to an existing tropical algebra package, but I am looking to generalize to other contexts - e.g., expressions involving more transcendental functions such as exponentiation and logarithm - in which the language of tropical algebra might be insufficient.) This is simpler in many ways, most notably due to the equivalence up to constants X+Y \sim \max(X,Y) of addition and maximum, which allows one to greatly simplify many expressions into monomial form (once one knows how things are ordered). Related to this (and your other comment), whereas an exact inequality can be refuted with a single example, an asymptotic estimate requires a parameterized family of counterexamples. One possible desirable feature - not currently implemented - is to have the tool output a specific such asymptotic counterexample whenever it is unable to verify the estimate. (This is presumably possible using dual linear programming to help locate the certificates, but I haven't seriously attempted to do this yet.) Reply 2 May, 2025 at 1:52 am Anonymous [] I mean existence of a violation means invalid inequality. Since you care about proving truth about only one inequality at a time, wouldn't Collins procedure typically run in time cubic or quartic in number of bits of required precision (assuming number of variables is O(1))? Reply 2 May, 2025 at 4:30 am Anonymous [] In the inequalities and probability discussions that Alexander Bogomolny posted on his blog https://x.com/CutTheKnotMath it was often clear that he viewed some of the problems as art of proof and art of intuition. Interestingly enough it now comes to a focus in foremost mathematical questions on AI abilities to discover mathematical results and evolving more in an art form Reply 2 May, 2025 at 6:12 am Lawrence Paulson [pic] For the special case of real asymptotics (including Landau symbols) an automated package is already available, thanks to the awesome Manuel Eberl. Its main mode of usage is to confirm (within Isabelle's proof kernel) a limit obtained elsewhere, e.g. through a computer algebra system, although it can also calculate limits itself. It can also prove that various properties hold in the limit, with a rather general notion of "in the limit" obtained using filters. Reply 2 May, 2025 at 6:47 am Anonymous [] would a formalization of the ideas sketched in https:// mathoverflow.net/questions/154373/differential-galois-number-theory help? Reply 2 May, 2025 at 6:57 am Anonymous [] You may be interedted in https://chatgpt.com/canvas/shared/ 6814dcdedae481919d4c964263d602a2 Reply 2 May, 2025 at 7:50 am - [789] Hi Terry, thanks for the wonderful post. I was the OP on that Math overflow question. My students have already built this tool to solve these types of questions. The first is through API calls to a math-specialized LLM, and the second by a modification of Alpha Geometry to questions like these. In particular, we are able to obtain full proofs to estimates like these in both questions. We will be emailing you shortly with more details. Thanks so much for the wonderful idea, we've had a wonderful year building these tools. Reply 2 May, 2025 at 9:20 am Terence Tao [d7f] That's great! I look forward to seeing the final products your group has produced. Reply 2 May, 2025 at 8:24 am Guanyuming He [9f6] Dear Prof Tao, A few noob questions: 1. Does a \lesssim b mean something like the Big-O in complexity theory, i.e., there exists C > 0 such that a \le Cb (except here we don't use absolute value, as everything is positive)? I asked because, as a non-native speaker, your sentence "we are willing to lose an unspecified constant in the estimates" seems to me meaning adding a constant a \le b + C instead. 2. To attack your example inequality by cases, we rely on the observation that a+b+c \sim \max(a,b,c). What about equality involving other operations, mult, exp, division, etc.; do they rely on such observations, too? And where could one find a list listing such an observation for each operation? Thank you, Guanyuming He Reply 2 May, 2025 at 8:33 am Terence Tao [d7f] 1: Yes; in this context, "constants" refer to "multiplicative constants" rather than "additive constants". 2: In general multiplicative operations (including raising to a fixed power) are easy to handle, since after taking logarithms, they become linear expressions, and in particular the question of determining whether one inequality implies another can be handled by linear programming tools. Reply 2 May, 2025 at 8:45 am Terence Tao [d7f] I am belatedly realizing that to make problems like this easy for brute-force computer tools to solve (as opposed to human verifiers), it makes sense to break up compound statements involving few variables into many atomic statements involving many variables, by giving each relevant term its own name. For instance, if one wants to prove that \max(a,b) * \min(c,d) \lesssim e, the helpful thing to do from a computer's point of view is to introduce new variables f = \ max(a,b), g = \min(c,d), h = \max(a,b) * \max(c,d), and reformulate the problem as that of establishing the inequality h \lesssim e subject to the relations f \sim \max(a,b), g \sim \min(c,d), h \sim f*g. The point is that case splitting becomes significantly more straightforward: for instance, the relation f \sim \max(a,b) can be decomposed into the relations f \gtrsim a and f \gtrsim b, together with one of f \sim a and f \sim b (and one has the option to split into cases to obtain one of these). My current implementation simply splits all cases at once, but one can do a more targeted approach of using linear programming to see whether the non-split constraints are enough to establish the desired bound, and if not perform one case split and recurse. (Another efficiency gain occurs if the same term appears multiple times in an expression, as it can be assigned just a single variable.) Reply 2 May, 2025 at 9:17 am Terence Tao [d7f] Another thing I am realizing is that while humans prefer to see the steps of a logical argument arranged in a linear sequence, with the justification of line n preferably located in a nearby preceding line (such as line n-1 or line n-2), computers have no such restrictions, and can easily manage large collections of hypotheses as an unordered set, with justifications drawn from arbitrary portions of such set as needed without any requirement to arrange things in any sort of linear order. In particular, the paradigm of proving estimates such as X \lesssim Y via chains of sub-estimates X \lesssim Z_1 \lesssim Z_2 \lesssim \dots \lesssim Z_n \lesssim Y, while helpful for human readers, may not be the right paradigm for proofs that are to be fully automated; I am leaning more towards just dumping a large number of relevant sub-estimates into an unordered set and calling a linear program at the end to obtain the desired conclusion from this unordered set of hypotheses. Reply 3 May, 2025 at 3:26 am Andrew Krause [8e5] I don't know what the right generalization of the earlier idea of phrasing everything in a tropical ring would be, but there may be something clever to be done in using such a formalism. Namely, given some way of representing the set of inequalities you are conceivably interested in, one could think about building a graph (possibly a tree) of inequalities which would then be itself a valuable database that could be queried quickly and expanded as needed (rather than needing to "re-prove" a given atomic inequality many times). This may be a naive idea, but something like this is used in some software packages that perform Symbolic Regression. Reply 2 May, 2025 at 8:57 am Evan Conway [317] For proving such asymptotic inequalities (with constant-loss), rule-based integration systems like Rubi are a promising blueprint to follow. Ideally, one could specify similar rules for inequalities, along with a list of known inequalities to try to reduce to. My intuition is that automatically finding a counterexample would be more difficult, but I am unsure of that. It may be tractable to use the same kind of rule-based system to automatically find a counterexample. Reply 2 May, 2025 at 9:26 am Terence Tao [d7f] Thanks for the pointer! Yes, I would like eventually to move to a rules-based framework, where one has the option to either (a) manually select rules to transform the proof state, (b) invoke a brute-force routine to try to automatically search the entire space of possible "moves", or (c) use some sort of AI to suggest a given rule to apply for any given state. A complex suite of estimates to be proven could then eventually be handled by some combination of (a), (b), and (c), for instance by brute forcing a few simple cases to discern some initial pattern, then (based on those preliminary findings) doing some medium difficulty cases by hand, calling an AI to then handle as many of the other cases as it can, and then finally study the last remaining cases manually. EDIT: actually a "tactic"-based framework may be a more accurate description of my long-term vision than a rules-based framework, using modern proof assistant languages such as Coq or Lean as models. (One could in fact try to encode such a verifier within say Lean metaprogramming, for instance leveraging existing tactics such as `linarith`... hmm, that actually sounds like a good way to go, now that I think about it.) Reply 3 May, 2025 at 11:25 am Dave Doty [5d6] This looks like a great idea! Someone above mentioned the sympy package; I'm not sure if you have experience with it. Looking through your repo, it seems plausible that you are manually reproducing some of what sympy can already handle. Not the asymptotics analysis to my knowledge... I just mean for instance your Variable and Expression classes seem very similar to sympy.Symbol ( https://github.com/sympy/sympy/blob/ 07449a736d039ce9bfca9bd55fdfc073fe4c05fb/sympy/core/symbol.py#L212) and sympy.Expr (https://github.com/sympy/sympy/blob/ 07449a736d039ce9bfca9bd55fdfc073fe4c05fb/sympy/core/expr.py#L47), and subclasses thereof, e.g., sympy.Mul similar to your Mul class (https: //github.com/sympy/sympy/blob/ 07449a736d039ce9bfca9bd55fdfc073fe4c05fb/sympy/core/mul.py#L91). Long-term, integrating such a tool directly into sympy would be great. In the meantime, it seems likely that your tool would be easier (both for you to develop and for users to use) using sympy objects, in order to leverage all the power sympy already has. For instance it can tell if an expression is a polynomial and then convert it to a polynomial object to do polynomial-related things, or render nice LaTeX-quality math expressions in a Juypyter notebook. For an example of the latter, see here: https://github.com/ UC-Davis-molecular-computing/ode2tn/blob/main/notebook.ipynb, where the differential equations rendered below the 2nd cell are from executing this function: https://github.com/ UC-Davis-molecular-computing/gpac/blob/ bf2f0ae1bcc4254e8b88909a0f481b11e126cd1b/gpac/ode.py#L876 I also left an issue on the GitHub issues page describing one source of potential bugs: https://github.com/teorth/estimates/issues/1 Reply 3 May, 2025 at 2:08 pm nunosempere2 [80e] Yeah, as a programmer I a) find it very impressive that you can do what the OP is doing from scratch, even with LLM assistance, but b) suspect it would be more meaningful/parsimonious to incorporate that functionality into an already existing project. Reply Leave a comment Cancel reply [ ] [ ] [ ] [ ] [ ] [ ] [ ] D[ ] For commenters To enter in LaTeX in comments, use $latex $ (without the < and > signs, of course; in fact, these signs should be avoided as they can cause formatting errors). Also, backslashes \ need to be doubled as \\. See the about page for details and for other commenting policy. << Stonean spaces, projective objects, the Riesz representation theorem, and (possibly) condensed mathematics Blog at WordPress.com.Ben Eastaugh and Chris Sternal-Johnson. Subscribe to feed. * Comment * Reblog * Subscribe Subscribed + [bd4bda] What's new Join 11,771 other subscribers [ ] Sign me up + Already have a WordPress.com account? Log in now. * Privacy * + [bd4bda] What's new + Subscribe Subscribed + Sign up + Log in + Copy shortlink + Report this content + View post in Reader + Manage subscriptions + Collapse this bar %d [b]