I agree only with the part about reconfiguring existing proofs. That's the value here. It is still likely very tedious to confirm what the LLMs say, but at least it's better than waiting for humans to do this half of the work.
For all topics that can be expressed with language, the value of LLMs is shuffling things around to tease out a different perspective from the humans reading the output. This is the only realistic way to understand AI enough to make it practical and see it gain traction.
As much as I respect Tao, I feel like his comments about AI usage can be misleading without carefully reading what he is saying in the linked posts.
> It is still likely very tedious to confirm what the LLMs say,
A large amount of Tao's work is around using AI to assist in creating Lean proofs.
I'm generally on the more skeptical side of things regarding LLMs and grand visions, but assisting in the creation of Lean proofs is a huge area of opportunity for LLMs and really could change mathematics in fundamental ways.
One naive belief many people have is that proofs should be "intelligible" but it's increasingly clear this is not the case. We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean.
This particular pattern of using state of the art work in two different areas (LLMs and theorem proving) absolutely has the potentially to fundamentally change how mathematics is done. There's a great picture on pp 381 of Type Theory and Formal Proof where you can easily see how LLMs can be placed in two of the most tricky parts of that diagram to solve.
Because the work is formally verified we can throw out entire classes of LLM problems (like hallucinations).
Personally I think strongly typed language, with powerful type systems are also the long term ideal coding with LLMs (but I'm less optimistic about devs following this path).
Perhaps you meant, "a decent amount of his recent work." He has been doing math long before LLMs, and is still regularly publishing papers with collaborators that have nothing to do with AI. The most recent was last week. https://arxiv.org/search/math?searchtype=author&query=Tao,+T
You are correct, I assumed context was implied, but I do mean "recent work with LLMs". Friends of mine where doing side projects with him about two decades ago, and I have a few of his books on my shelf, so yes, I am aware that Terry Tao was doing work in mathematics prior to the advent of LLMs.
> I don't believe that's what's happening in this specific example (and am probably wrong), but this is where a lot of Tao's enthusiasm lies.
It absolutely is. With the twist that ChatGPT 5.2 can now also "explain" an AI-generated Lean proof in human-readable terms. This is a game changer, because "refactoring" can now become end-to-end: if the human explanation of a Lean proof is hard to grok and could be improved, you can test changes directly on the formal text and check that the proof still goes through for the original statement.
> One naive belief many people have is that proofs should be "intelligible" but it's increasingly clear this is not the case.
That's not a naïve belief. Intelligible proofs represent insight that can be applied to other problems. If our only proof is an opaque one, that means we don't really understand the area yet. Take, for example, the classification of finite simple groups (a ten-thousand-page proof): that is very much not a closed area of research, and we're still discovering new things in the vicinity of the problem.
If you consider the statement that perfect play by both sides in checked results in a draw to be the statement of a theorem, then the proof is 237GB compressed :) And verifying it requires quite a lot of computation.
> We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean.
I'm not aware of any of these. There's some SAT-like results that were not verified in Lean at that sort of scale, but Lean proofs of individual problems are nowhere near that. For example, Mathlib (think a Lean4 math stdlib) is 6GB including compilation artifacts, and iirc <100MB text.
> One naive belief many people have is that proofs should be "intelligible" but it's increasingly clear this is not the case.
That’s one of the main reason why I did not pursue an academic math career. The pure joy of solving exam problems with elegant proofs is very hard to get on harder problems.
Cheers, I thought I was the only person like this :) (also didn’t tie it to my anxiety, but it’s extremely obvious in retrospect. This is too short and elides the own kind of comfort part, but I guess it means I can’t spin out, ruminating on or creating other problems, when I have stuff right here to complain about!)
> The engineer is forced into manual correlation: jumping between dashboards, aligning timelines by eye, [and] inferring causality from coincidence
I just generate a random UUID in the application and make sure to log it everywhere across the entire stack along with a timestamp.
Any old log aggregator can give me an accurate timeline grouped by request UUID across every backend component all in one dashboard.
It's the very first thing that I have the application do when handling a request. It's injected it at the log handler level. There's nothing to break and nothing to think about.
So, I have no problem knowing precise cause and effect with regard to all logs for a given isolated request, but I agree that there may be blips that affect multiple requests (outages, etc.). We have synthetic tests for outages though.
I too am struggling to understand what this tool does beyond grouping all logs by a unique request identifier.
founder at base14 here, the company that is building Scout. Thanks for the feedback. we do something similar for tracing as well, but pgX does a bit more than that - engineers should be able to trace (like you mention) and see and analyse the condition of the DB. for eg - correlate query slowdown to locks, vacuums etc. all on one screen, or a couple of clicks. We are building some specialised explorers like pgX for postgres. Essentially we are building telemetry readers for components that send relevant metrics and logs through to a telemetry data lake. for each component/domain we find from experts what they look at for analysis and incidents, and bring that to a full stack "unified" dashboards/mcp.
Scout is our otel-native observability product (data lake, UI, alerts, analytics, mcp, the works).
what we call pgX in the blog is an add-on to Scout.
If you use OpenTelemetry, it basically does exactly that and you can send traces to some self-hosted FOSS visualizer, like Jaeger. You can also easily get the UUID of the spans/traces and have your logger automatically put them in every log message.
I have no doubt there are many tools, but I specifically mentioned my solution because it doesn't require any tools at all and just a matter of log hygiene.
They spend the whole page talking about a scenario that I've only seen happen in production when there were no app devs involved and people are allergic to writing a log format string let alone a single line of code.
This is a great PR move for Bose in a market that doesn't care about name brands like it used to. Maybe they can win some customers back and be considered cool again.
Yeah it's not a CRT simulator. It's a minimal shader to give a CRT-like vibe. Minimal as in the least amount of processing, so it performs well on older devices.
A better demo would correlate the pixelization of the source with the settings in the sidebar. Doesn't even have to be part of the shader, but would convey the effect better. The animated shapes toggle really kills the illusion.
The animated shapes are off by default. They're there only so you can see how the settings affect red, green, and blue individually and in motion. For example with some settings the scanlines tend to disappear on red when in motion.
Franks and beans are not the best meal on the cheap. Sounds more expensive than cooking fresh and you're missing out on better nutrition.
For the most bang for your buck you want to be eating less expensive real protein like chicken and pork and filling up on salads. Limit carb intake from beans and other starches. Prefer fruit for carbs because it has fiber and vitamins you can't get anywhere else.
You are preposterously out-of-touch with reality here. "Filling up on salads" is healthy but it is FAR from the most "bang for your buck". And are seriously trying to say that beans aren't a good source of fiber and vitamins?
Sure you shouldn't eat hot dogs and baked beans three meals a day every day but you are absolutely out of your mind if you think cheap sausage and canned beans are bad to have in the house when you are struggling.
I am reading what you wrote and disputing it but you don't seem to want to hear it.
I am saying that denying the sale of all "ULTRA PROCESSED" foods to people receiving food assistance is NOT helpful because deciding what counts as "ultra-processed" is too messy and imprecise.
You are trying to split hairs over the most cost-effective struggle meals.
I can indulge you.
---
Perdue Young Whole Chicken Fresh (~5lb) = $12.49
Oscar Mayer Original Uncured Turkey Chicken & Pork Wieners (10 count) $4.49 +
3x Bush's Best Original Baked Beans (16 oz.) $7.47 ($2.49 ea.) = 11.96 total
You eat half a can of beans and one hot dog per meal. That's six meals and four extra hot dogs you can do whatever else you want with.
You can definitely get six meals out of a whole chicken but it's going to be a lot more work plus the additional 50c cost (and that's ignoring the value of the four extra hot dogs). 1 hot dog + 8oz of beans is going to be a fairly similar portion to 1/6th the recoverable meat from a 5lb bird.
It should obviously go without saying but, since you seem to be a stickler, I should point out that there is nothing stopping you from eating chicken one week then frank & beans the next. Variety is the biggest part of a healthy diet.
Your body doesn't care about the weight of the food nor the quantity of items in the package.
You eat calories and process nutrients. You can make a lot more meals and a wider variety of recipes with a whole chicken than a pack of hot dogs.
Anyone who shops like you described is not being efficient with their money as long as they have their own kitchen. Poverty is a lot of possible scenarios. I'm not saying they're dumb or anything.
Nutrition is hard to think about when tempted by the modern convenient grocery store with limited money. Unit price has a way of messing with your head. I also get the practicality of having packaged and shelf stable food when you lack access to a freezer and can't stay somewhere for too long. It is what it is.
"What meals can I make with a given amount of money?" is a reasonable way to shop.
You said:
> Franks and beans are not the best meal on the cheap. Sounds more expensive than cooking fresh and you're missing out on better nutrition.
> For the most bang for your buck you want to be eating less expensive real protein like chicken and pork and filling up on salads.
I gave you math on how you can take the money you would have spent on chicken and get essentially the same "bang for your buck" by spending it instead on canned beans and cheap sausage for the protein portion of your meals.
It is completely reasonable to allow people who receive money for food assistance to buy hot dogs.
It is completely unreasonable to disallow people who receive money for food assistance from purchasing anything "Ultra Processed" because "Ultra Processed" is a category too broad and loose to determine whether or not a given food item is "healthy".
Beans are legitimately one of the most balanced foods out there. Yes, they have carbs (but they're more complex than the simple sugars in fruit), they also have a lot of fiber, protein and several key micro-nutrients. Not to mention, most people on SNAP have kids and good luck getting them to eat salads.
