Posts by tao@mathstodon.xyz
(DIR) Post #ApSAvJXbzbujJTmuzg by tao@mathstodon.xyz
2024-12-26T21:14:41Z
0 likes, 1 repeats
One of my papers got declined today by the journal I submitted it to, with a polite letter saying that while they found the paper interesting, it was not a good fit for the journal. In truth, I largely agreed with their conclusions, and the paper is now submitted to a different (and hopefully more appropriate) journal.Rejection is actually a relatively common occurrence for me, happening once or twice a year on average. I occasionally mention this fact to my students and colleagues, who are sometimes surprised that my rejection rate is far from zero. I have belatedly realized our profession is far more willing to announce successful accomplishments (such as having a paper accepted, or a result proved) than unsuccessful ones (such as a paper rejected, or a proof attempt not working), except when the failures are somehow controversial. Because of this, a perception can be created that all of one's peers are achieving either success or controversy, with one's own personal career ending up becoming the only known source of examples of "mundane" failure. I speculate that this may be a contributor to the "impostor syndrome" that is prevalent in this field (though, again, not widely disseminated, due to the aforementioned reporting bias, and perhaps also due to some stigma regarding the topic). So I decided to report this (rather routine) rejection as a token gesture towards more accurate disclosure. (1/2)
(DIR) Post #ApSAvRovD8VuzTwr5M by tao@mathstodon.xyz
2024-12-26T21:19:04Z
0 likes, 0 repeats
With hindsight, some of my past rejections have become amusing. With a coauthor, I once almost solved a conjecture, establishing the result with an "epsilon loss" in a key parameter. We submitted to a highly reputable journal, but it was rejected on the grounds that it did not resolve the full conjecture. So we submitted elsewhere, and the paper was accepted. The following year, we managed to finally prove the full conjecture without the epsilon loss, and decided to try submitting to the highly reputable journal again. This time, the paper was rejected for only being an epsilon improvement over the previous literature! (This paper was also submitted elsewhere, and accepted; and I have subsequently published in that highly selective journal since. Being an editor myself, and having had to decline some decent submissions for a variety of reasons, I find it best not to take these sorts of rejections personally, and move on to other journals, of course after revising the paper to address any issues brought up by the rejection.) (2/2)
(DIR) Post #ApuUUsAqZZRUQX49Tc by tao@mathstodon.xyz
2025-01-09T15:28:40Z
0 likes, 1 repeats
An illustration of survivor bias: yesterday the speaker in our seminar asked of anyone was affected by the ongoing fires. Everyone present assured the speaker that they were not significantly impacted.Attendance was about half of the normal size.
(DIR) Post #Au5sZ0zMtDZw2nvCFc by tao@mathstodon.xyz
2024-11-21T18:52:30Z
1 likes, 0 repeats
As of yesterday, the Equational Theories Project https://teorth.github.io/equational_theories/ has (provisionally) attained its aim of resolving all 22028942 implications between the 4694 equational laws of magmas involving at most four multiplication operations. We are not fully done yet - there are 52 resolutions that currently only have a human-readable proof but not a Lean-formalized proof (actually, there are a few that are not even human-readable, but are instead computer-generated by some non-Lean program) - but it should now just be a matter of time before we can declare final success in which the full implication graph is completely formalized in Lean. As such, we are now beginning the process of writing up the results.The full implication graph is too large to easily visualize, but we have tools to inspect fragments of it at a time: for instance here is a graph of all the laws that are implied by Equation 854, x = x ◇ ((y ◇ z) ◇ (x ◇ z)): https://teorth.github.io/equational_theories/graphiti/?render=true&highlight_red=854&implies=854 . The Equation Explorer tool at https://teorth.github.io/equational_theories/implications/ lists all the equations, their implications, and various commentary on some selected equations.There are various spinoff projects that are still ongoing, for instance to work out the analogous implication graph when restricted to finite magmas, or to perform data analysis on the graph and see if there are any interesting features. We've also learned a lot of lessons on how to run a large collaborative math research project, which we will report in our paper and which we hope will be useful for future such projects. Additionally, I also hope the implications here could serve as benchmarks for future AI math tools.
(DIR) Post #AuTn7yWFGa9tKs5NuS by tao@mathstodon.xyz
2025-05-25T14:42:37Z
0 likes, 1 repeats
The #NSF has reduced spending on the basic sciences by 50% or more in 2025, with similar cuts proposed for next year as well. For instance, through to May 21 of this year, the funding awarded to the mathematical sciences is currently $32 million, compared to the 10-year average of $113 million. These are of course large numbers for an individual person; but with the US population of 340 million, this amounts to spending less than 22 cents per American per year on basic #mathematics research, compared to the 10-year average of 80 cents per American per year. https://www.nytimes.com/interactive/2025/05/22/upshot/nsf-grants-trump-cuts.htmlI myself have been fortunate to be supported by a small fraction of this 80 cents for almost the entirety of my professional career, allowing me to conduct research in the summer, invite speakers to my department, and to support graduate students. For now, I can continue these activities at a minimal level using by existing (and relatively modest) NSF grant https://www.nsf.gov/awardsearch/showAward?AWD_ID=2347850 , but already I do not have the resources to put into any future long-term projects. For instance, my experiments with using new technologies for mathematical workflows are currently being conducted purely by myself together with contributions from unpaid online volunteers; I am applying for funding from several sources to scale these projects up beyond a proof-of-concept level, but I am expecting the process to be extremely competitive. (1/3)
(DIR) Post #AuTn86kMfyCqqykm1o by tao@mathstodon.xyz
2025-05-25T14:43:05Z
0 likes, 0 repeats
Basic mathematical research pursues questions that are often quite far from actual practical application; but they contribute, in a largely invisible way, to the broader research ecosystem that eventually does generate such application. For instance, consider the problem of packing spheres into space as efficiently as possible - a question first proposed by Kepler in 1611. At a practical level, the solution to this problem has been "known" to greengrocers for centuries - one should stack the spheres in a hexagonal close packing. But mathematicians spent decades to work out how to establish the optimality of this packing, culminating in a formally verified proof in 2012.Mathematicians also explored variants of this sphere packing problem in other geometries than three-dimensional Euclidean space: for instance in higher dimensions, with the famous recent breakthroughs of Viazovska in 8 and 24 dimensions, or in more discrete geometries over finite fields. Such curiosity-driven questions appear to lack immediate application - nobody had a need to pack eight-dimensional oranges together, for instance. (2/3)
(DIR) Post #AuTn8FLsgMy9XeMqcC by tao@mathstodon.xyz
2025-05-25T14:47:08Z
0 likes, 0 repeats
But when cellphone adoption became widespread, it became necessary to figure out how to efficiently encode the signals of multiple cellular devices in the wireless spectrum in such a way that they do not interfere with each other. As it turns out, many of the mathematical techniques and insights generated by exploring these discrete and high-dimensional versions of the sphere packing problem have been of immense value for this problem - not just in the "positive" sense of designing efficient signal encoding methods, but also in the "negative" sense of also giving theoretical upper bounds on such efficiency, thus setting the right benchmarks to evaluate progress, and to avoid wasting resources on attempting encodings that are mathematically impossible. (As a side note, the successful formalization of the proof of the Kepler conjecture has also inspired and informed many further collaborative formal projects, including my own experiments in this area, even if those projects do not directly involve sphere packing.)Such contributions to tangible technological advances are subtle and indirect; but without such basic research, many such advances would have taken far longer to be developed, and some may not have been pursued at all. The cuts to funding for such reseearch - which will particularly impact the next generation of researchers - may save a few cents a year in the short term, but greatly reduce the capacity to solve many challenging technological problems of significant real-world impact in the future. (3/3)
(DIR) Post #Av63QtQyEsN49B353w by tao@mathstodon.xyz
2025-06-13T18:57:43Z
1 likes, 0 repeats
Maryna Viazovska is launching a project to formalize a proof of her well-known result that the E_8 lattice is the optimal sphere packing in eight dimensions. The announcement can be found at https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Sphere-Packing/with/523951357 where you can also find a talk by Viazovska describing the project.Among other things, the project will develop some of the classical theory of modular forms and complex analysis, which is only partially in Lean's Mathlib at present. For instance, Cauchy's theorem is only currently available for rectangular contours, which means that the valence formula for modular forms (which is usually proven using Cauchy's theorem applied to a non-rectangular contour) is not yet formalized.
(DIR) Post #AvpUUioTEcgiNXSvuy by tao@mathstodon.xyz
2025-07-05T15:57:53Z
0 likes, 0 repeats
"In the end, the Party would announce that two and two made five, and you would have to believe it. It was inevitable that they should make that claim sooner or later: the logic of their position demanded it. Not merely the validity of experience, but the very existence of external reality, was tacitly denied by their philosophy. The heresy of heresies was common sense. And what was terrifying was not that they would kill you for thinking otherwise, but that they might be right. For, after all, how do we know that two and two make four? Or that the force of gravity works? Or that the past is unchangeable? If both the past and the external world exist only in the mind, and if the mind itself is controllable—what then?" - George Orwell, "Nineteen Eighty-Four". (1/6)
(DIR) Post #AvpUUkK3cfY53nFfn6 by tao@mathstodon.xyz
2025-07-05T15:58:03Z
0 likes, 0 repeats
In modern mathematics we take it for granted that there is a consensus standard of truth that virtually all mathematicians subscribe to, and which permit even the bitterest mathematical disputes to be resolvable by breaking down the mathematical arguments into atomic steps and comparing them against the (nearly universally accepted) axioms of mathematics. I myself experienced this first-hand back in 2015, when Edward Nelson, a renowned logician, announced a proof that Peano Arithmetic was in fact logically inconsistent; this was a shocking claim, and the argument initially looked quite serious; but Daniel Tausk and I found an error in the argument, which Nelson graciously acknowledged, withdrawing the claim. (The discussion where this took place can be found at https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html .) Despite Nelson's quite non-mainstream views on the consistency of arithmetic, he still firmly believed in the consensus standard of mathematical truth, even going so far as building his own proof assistant in which he had already partially formalized his argument (although, crucially, the most problematic portions of his argument had not actually been formalized). (2/6)
(DIR) Post #AvpUUlWr8ZNenmFPNY by tao@mathstodon.xyz
2025-07-05T15:58:18Z
0 likes, 0 repeats
This ability to arrive at consensus by recognizing an objective standard of truth that all personal or political opinions are subordinate to is increasingly rare outside of mathematics, to the point where many non-mathematicians may not even be aware that such a epistemological framework is even possible: in so many spheres of discourse nowadays, it has become normalized to view objective standards primarily as ideological tools, cited to support one's preferred arguments or to attack one's opponents if they align with one's views, but ignored or discredited if they do not. The idea of a leading figure actually changing their views because the objective data was consistently pointing to a different conclusion has become almost quaint. (3/6)
(DIR) Post #AvpUUmk0d9UoYrPQWG by tao@mathstodon.xyz
2025-07-05T15:58:47Z
0 likes, 0 repeats
And even in mathematics, our consensus standard (which was painfully acquired over many centuries of foundational debate, particularly during the "crisis in foundations" in the early twentieth century) is not completely universal and invulnerable. Consider for instance the affair of Mochizuki's claimed proof of the abc conjecture from 2012, which has not been withdrawn; the usual consensus-building steps of having good-faith technical discussions about key definitions and claims have failed to take place despite some valiant efforts, and what discussion remains has become increasingly personal and unproductive. (In particular, there is no viable path currently to formulating the arguments in a way that could conceivably be verifiable by a formal proof assistant.) (4/6)
(DIR) Post #AvpUUnyE3mSiNF4IJk by tao@mathstodon.xyz
2025-07-05T15:58:58Z
0 likes, 0 repeats
More recently, we face the real and disturbing possibility that certain directions of mathematical inquiry - for instance, in developing reliable statistical tests for electoral integrity - may not only be defunded by public science agencies, but have their mathematical conclusions actually overruled by political ideology. Even if the supremacy of the objective mathematical standard of truth is technically acknowledged, it can still become weaponized: mathematical results which go against the prevailing ideology could be relentlessly critized for even the slightest typo or technical flaw in the presentation, whereas results that support this ideology could be uncritically embraced even they contain substantial gaps or ambiguities in interpretation. (5/6)
(DIR) Post #AvpUUoqSo7qb5SRbrE by tao@mathstodon.xyz
2025-07-05T15:59:10Z
0 likes, 0 repeats
One potential bulwark against such politicization of mathematical truth is the broader adoption of formal proof verification, though even here there are some (fortunately still quite theoretical at present) potential "exploits", for instance through subtly altering the definitions of key concepts in Lean's core "Mathlib" library. (See this recent talk https://www.newton.ac.uk/seminar/46706/ "Can Mathematics Be Hacked? Infrastructure, Artificial Intelligence, and the Cybersecurity of Mathematical Knowledge" by Fenner Tanswell.) Still, I view an increased acceptance and deployment of formal methods as a net positive in this regard, even if it is not a "silver bullet".More generally, I think it is important to acknowledge just how precious the consensus objective standard of mathematical truth is, and how important it is to defend it. (This is not to say that such foundational matters should be completely immune from criticism or debate; but such discussion should be in good faith and grounded by genuine philosophical concerns, rather than driven by some external political agenda.) (6/6)
(DIR) Post #Ax6LaIqpaihTQyuo2y by tao@mathstodon.xyz
2025-08-12T17:45:13Z
1 likes, 0 repeats
Somewhat related to my previous post; there is apparently an AI startup offering "personalized video tutorials" with AI avatars of several people including myself. Again, for the record, I am not involved in any such project, and any such use of my likeness was without my consent.
(DIR) Post #AxJVaWpd8WgXOIZwmm by tao@mathstodon.xyz
2025-08-18T15:45:37Z
0 likes, 0 repeats
I wrote an op-ed on the world-class STEM research ecosystem in the United States, and how this ecosystem is now under attack on multiple fronts by the current administration: https://newsletter.ofthebrave.org/p/im-an-award-winning-mathematician
(DIR) Post #AxVzlD3UKmAZlKaaMS by tao@mathstodon.xyz
2025-08-25T01:30:01Z
0 likes, 0 repeats
Developers of AI tools often focus on trying to create a useful "success mode" for their tool, where the tool accomplishes the task that the user requested. But having a clearly identified "failure mode" is equally important, and does not always receive a corresponding amount of attention.To give an analogy: if one is looking for some piece of information (e.g., obscure quote from a film that one has forgotten the name of), one can type some half-remembered version of the quote into a search engine and see what happens. If one is lucky, one activates the "success mode" where a useful hit is returned. Or, one can have a clear "failure mode" in which some message along the lines of "no relevant matches found" is shown, and one can either switch to a different way of searching for the information, or abandon the search entirely. However, there are also more ambiguous "intermediate modes" in which the search engine returned some hits that partially matched one's query, but do not seem to be exactly what one wants. This can lead to a somewhat frustrating and time-wasting exercise of investigating false leads and continuing fruitless queries (which could happen for instance if one had misremembered a key detail of the information one is trying to search for, and misconfiguring the search queries accordingly). This is often a significantly worse user experience than if the search engine had simply displayed a "failure mode" immediately. (1/3)
(DIR) Post #AxVzlEMfSx6bp6ZPtY by tao@mathstodon.xyz
2025-08-25T01:30:14Z
0 likes, 0 repeats
In contrast, AI chatbots are usually tuned to avoid a "failure mode" as much as possible, at the expense of increasing the occurrence of "intermediate modes" where the chatbot response looks potentially useful, and invites further interaction from the user, but is not exactly providing what the user wants, and could contain hallucinations or some fundamental misunderstanding of the task that would take significant effort to uncover. Paradoxically, such tools may become significantly more useful if they simply reported that they were unable to provide a high quality answer to a query in such cases.A comparison may be drawn with the increasingly advanced, but stringently verified, "tactics" used in a modern proof assistant such as Lean. I have been experimenting recently with the new tactic `grind` in Lean, which is a powerful tool (inspired more by "good old-fashioned AI" such as satisfiability modulo theories (SMT) solvers, than modern data-driven AI) to try to close complex proof goals if all the tools needed to do so are already provided in the proof environment; roughly speaking, this corresponds to proofs that can be obtained by "expanding everything out and trying all obvious combinations of the hypotheses". When I apply `grind` to a given subgoal, it can report a success within seconds, closing that subgoal in a Lean-verified fashion and allowing me to move on to the next subgoal. But, importantly, when this does not work, I quickly get a "`grind` failed" message, in which case I simply delete `grind` from the code and proceed by a more pedestrian sequence of lower level tactics. (2/3)
(DIR) Post #AxVzlFYl1UN1WtEaNU by tao@mathstodon.xyz
2025-08-25T01:30:30Z
0 likes, 0 repeats
While `grind` does have some additional tuneable parameters and options that I could try to tweak to try to coax it to work, I am finding that the optimal way for me to use this tool is not to try to explore too much the "intermediate modes" in which I try to repeatedly reconfigure the tool: if I cannot use `grind` to close the goal after one or two such attempts, I simply move on. I still find the tool to be a non-trivial time-saver in many contexts, but in some circumstances the way it saves time is by promptly signaling that it is not the appropriate tool for the task at hand.Are there any prominent examples of chatbots that are tuned to report failure modes instead of intermediate modes when the confidence level of their answer is low? I hypothesize that these may actually be a more useful and less frustrating type of assistant to incorporate into complex workflows, despite being seemingly less "powerful". (3/3)
(DIR) Post #B0fBG4rawkokBSNhLM by tao@mathstodon.xyz
2025-11-27T06:33:08Z
1 likes, 0 repeats
This two-dimensional image has been circulating recently as an metaphor for the current state of AI technology. It is admittedly an improvement over one-dimensional narratives in which AI development is presented as a linear progression from sub-human intelligence to super-human intelligence. However, it is still a significant oversimplification. The space of cognitive tasks is not well modeled by either one-dimensional or two-dimensional spaces, but is instead extremely high-dimensional. There are now indeed many directions in this high-dimensional space in which AI tools can, with minimal supervision, achieve better performance than human experts. But, as per the "curse of dimensionality", such directions still remain very sparse. Also, human performance is also very spiky and diverse; representing this by a single round disk or ball is also somewhat misleading.In high dimensions, the greatest increase in volume often comes from taking combinations of smaller, spikier sets. A team of humans working together, or humans complemented by a variety of AI tools, can achieve a significantly greater performance on many tasks than any single human or AI tool could achieve individually, particularly if they are strong in "orthogonal" directions. On the other hand, the choice of combination matters: the wrong combination could lead to a misalignment between the objective and the actual outcome, in which the stated goal may be nominally achieved, but at the cost of several unwanted secondary effects as well.TLDR: the topic of intelligence is too high-dimensional for any low-dimensional narrative to be perfectly accurate, and one should take any such narratives with a grain of salt.