teorth.bsky.social - Profile | ThreadSky | a Reddit-style client for Bluesky

A third video in my occasional series on #Lean4 formalization workflows, this time focusing on how relying extensively on #GitHubCopilot fares against standard "epsilon delta" type problems in analysis. www.youtube.com/watch?v=c1ix...

submitted 1 day ago • 0 comments

A followup to my previous video, in which I now see how #Claude and #o4mini do at formalizing a slightly different proof of the same algebraic implication, after being given the initial informal and formal proofs as reference. www.youtube.com/watch?v=zZr5...

submitted 5 days ago • 1 comment

As an experiment, I tried to use automated tools to formalize (in as "mindless" a fashion as possible) a one-page human written proof into Lean. You can watch the results here: www.youtube.com/watch?v=cyyR...

submitted 7 days ago • 2 comments

DARPA's "Exponentiating mathematics" (expMath) program, which is launching a challenge to develop and evaluate "AI collaborators" for assist in decomposing and formalizing informal mathematical proofs, is now taking short abstract proposal submissions: sam.gov/opp/869c8d73...

submitted 17 days ago • 5 comments

After 200 days, we finally have 100% completion on the primary goal of the Equational Theories Project to formally resolve >22 million implications between 4694 equational laws, using modern proof assistants, collaboration platforms, and automated theorem provers. teorth.github.io/equational_t...

submitted 34 days ago • 2 comments

A new #CosmicDistanceLadder post, on intriguing hints from the DESI survey data that suggests that the cosmological constant (aka "dark energy) might not, in fact, be constant after all. www.instagram.com/p/DIP0yy5oDUu

submitted 38 days ago • 0 comments

A new #CosmicDistanceLadder post on why lunar and solar eclipses tend to come in pairs (for instance, the solar eclipse next week is paired with the lunar eclipse from last week). www.instagram.com/p/DHkS3EcA40L

submitted 55 days ago • 1 comment

Cosmic Distance Calibration xkcd.com/3066

submitted 58 days ago • 100 comments

A new #CosmicDistanceLadder post, on how the recent lunar eclipse from the vantage point of the Earth becomes a solar eclipse from the vantage point of the Moon: www.instagram.com/p/DHR1tuWonDR/

submitted 62 days ago • 2 comments

Lunar eclipses, such as the one yesterday, were one of the earliest pieces of scientific evidence that the Earth was basically a round sphere, already known to Aristotle: regardless of the position of the eclipse in the light sky, the shadow of the Earth on the Moon was always circular.

submitted 65 days ago • 1 comment

A new post on my #CosmicDistanceLadder Instagram with Tanya Klowden on the parallels (but also differences) between ancient Greek and ancient Indian astronomy. www.instagram.com/p/DGzJs02AbBA

submitted 74 days ago • 1 comment

While serving on PCAST we interacted with this group. They did great work providing efficient digital services to the federal government and cited them as an excellent model for other potential service needs such as science communication: bidenwhitehouse.archives.gov/pcast/briefi...

submitted 77 days ago • 0 comments

I am happy to announce that the Kakeya set conjecture, one of the most sought after open problems in geometric measure theory, has now been proven (in three dimensions) by Hong Wang and Joshua Zahl! arxiv.org/abs/2502.17655 I discuss some ideas of the proof at terrytao.wordpress.com/2025/02/25/t...

submitted 81 days ago • 0 comments

I wrote a blog post on how a piece of pure mathematics - the development of the landscape function in PDE - played a part in realizing noticeable savings in household energy bills due to improved LED lighting technology: terrytao.wordpress.com/2025/02/23/c...

submitted 83 days ago • 2 comments

This was a very enjoyable collaboration with @3blue1brown.bsky.social . Tanya Klowden and I are continuing to work on developing this material into a popular science book; we will share our progress on our Instagram at www.instagram.com/cosmic_dista...

submitted 84 days ago • 3 comments

The American Mathematical Society has also started a page to coordinate support for professional mathematics, so far focusing on executive orders impacting the National Science Foundation: www.ams.org/government/g...

submitted 85 days ago • 1 comment

A letter of support for the NIH funding of biomedical research, and the damage wrought by imposing severe caps on indirect costs: docs.google.com/forms/d/1Agz...

submitted 85 days ago • 2 comments

Part one of a collaboration with @3blue1brown.bsky.social on presenting the mathematics of the cosmic distance ladder in an accessible fashion.

submitted 99 days ago • 2 comments

#DARPA just announced a forthcoming program entitled "Exponentiating Mathematics", focusing on challenges to auto-formalization (and auto-decomposition of large proofs into small lemmas). The preliminary announcement (still short on many details) can be found at sam.gov/opp/4def3c13...

submitted 100 days ago • 3 comments

The "Lean for Mathematicians" workshop, aimed at training graduate students and postdocs in the use of the Lean proof assistant language for mathematics, runs June 16-27 2025 and is currently taking applications. sites.google.com/view/simonsl...

submitted 102 days ago • 2 comments

Launching the Analytic Number Theory Exponent Database (ANTEDB) at github.com/teorth/expdb to systematically collect known results in the literature on such exponents. More info (and a companion paper) at terrytao.wordpress.com/2025/01/28/n...

submitted 109 days ago • 0 comments

A brief update on my #CosmicDistanceLadder instagram with Tanya on the fires that have affected (one of our) home cities. (But the sky is much, much bluer today.) www.instagram.com/p/DEyx7o_OFLz

submitted 124 days ago • 0 comments

A #CosmicDistanceLadder on how Christmas in Australia is inverted in many ways from Christmas in the Northern hemisphere, and how the parallax differences were once important in climbing that distance ladder. www.instagram.com/p/DEExnvvRkCQ

submitted 142 days ago • 0 comments

A new #CosmicDistanceLadder post on the winter/summer solstice in the Northern/Southern hemisphere yesterday: www.instagram.com/p/DD1c47nIKJ2 (One can also refer to this solstice as the Southern solstice - the time of year when the Sun is at its southernmost, regardless where one is on the Earth.)

submitted 147 days ago • 1 comment

I wrote a blog post on how quaternions can be used to derive the equations of spherical geometry, as well as the sunrise equation relating the time of sunrise or sunset to one's latitude and the declination of the Sun. terrytao.wordpress.com/2024/12/19/q...

submitted 150 days ago • 0 comments

My #math department at #UCLA is now advertising for an additional tenure-track assistant professor position as part of UCLA's HSI (Hispanic Serving Institution) initiative: recruit.apo.ucla.edu/JPF10045 . The deadline for applications is Jan 20, 2025.

submitted 151 days ago • 1 comment

#PCAST (the President's Council of Advisors on Science and Technology, on which I currently serve) has released its report on groundwater resilience, and how the federal government can assist state, local, and tribal management efforts. www.whitehouse.gov/pcast/briefi...

submitted 153 days ago • 0 comments

AIMO, the Artificial Intelligence Mathematical Olympiad, is in its second year, with a new and harder set of problems. It has just awarded a prize of $20,000 to Md Boktiar Mahbub Murad for being the first person to write a program that solves 20/50 of the problems and make it freely available.

submitted 156 days ago • 1 comment

New essay: "How to be a wise optimist about science and technology?" michaelnotebook.com/optimism/ind...

submitted 168 days ago • 7 comments

Tanya Klowden and I visited the Getty Museum to see some scientific and artistic exhibits relevant (mostly from the ancient Greek, Arab, and medieval eras) to our Cosmic Distance www.instagram.com/p/DDgGAyEI5eR/

submitted 156 days ago • 0 comments

Renaissance Philanthropy and XTX Markets have launched a $9.2 million "AI for Math fund" to support the development of new AI tools as long-term building blocks to advance mathematics. (I have agreed to serve on the advisory board for this fund.) renaissancephilanthropy.org/news-and-ins...

submitted 164 days ago • 2 comments

AI for Mathematics and Theoretical Computer Science, a workshop hosted jointly by the Simons Institute for the Theory of Computing and the Simons Laufer Mathematical Sciences Institute, will be held in Berkeley at April 7-11, 2025. simons.berkeley.edu/workshops/si...

submitted 167 days ago • 1 comment

When can a sum of reciprocals of natural numbers sum to a rational number? There are many unsolved problems in this area, by Erdős and others. With Vjeko Kovac, we have been able to resolve some open questions and make progress on others: terrytao.wordpress.com/2024/11/27/o...

submitted 170 days ago • 2 comments

The second Artificial Intelligence Mathematical Olympiad #AIMO challenge is closing in on the 20/50 threshold (on the public leaderboard) needed to trigger the $20,000 "Early Sharing Prize". Currently, the best submissions are at 18/20: www.kaggle.com/competitions...

submitted 170 days ago • 2 comments

A new post by my co-author Tanya Klowden on our "Cosmic distance ladder" instagram, on the constellations on the ecliptic (most familiar to western astrology as the signs of the Zodiac), as viewed by native Americans prior to European colonization. www.instagram.com/p/DC8gvXXxtfw

submitted 170 days ago • 0 comments

Tanya Klowden and I have set up an instagram to record various #astronomy stories we have gathered during the process of writing a forthcoming book on the cosmic distance ladder. Our latest post, on the "mini-moon" that briefly visited our neighborhood, is now up: www.instagram.com/p/DC08k17xZqB

submitted 173 days ago • 2 comments