isotypic

I mean, my reaction to God coming down and saying they were bored of being God and instead they would just sit around and answer all of the mathematician's questions would largely be the same, so yes, who cares if its God's book or the machines Xeroxed copy?

"The Book" is more interesting to me if I am the one coming up with the ideas to fill it in. Maybe this is a bit egotistical, but I'd like to think it is allowed to have a desire that you, personally, are contributing to something in a meaningful way. Like, if you are on a sports team, it'd be more fun to win a game if you were on the field than if you were benched, and I think that's okay. And ultimately I don't find dredging for proofs from an LLM particularly meaningful, nor do I see it as a particularly personal contribution, as anybody else could have done the exact same thing with the same prompt.

This isn't to say I wouldn't love to read the proofs in "The Book" for problems I care about, I just think I'd eventually get bored of only reading. And so its hard to be enthusiastic when this book is being built through an LLM.

LLMs applying the ideas to problems I'm trying to solve is exactly what I said I wasn't interested in, actually. Because the LLM doing this for me reduces back to me simply reading from the textbook, only now I have no problems I'd be interested in applying things to since, again, they're already in the textbook.

I cannot quite share your enthusiasm. The clearest analogy that I can think of to try to explain why I feel this way is that it seems there will eventually be a phantom textbook of all of mathematics contained in the weights of an LLM; every definition, every proof, etc; and the role of a mathematician is going to be reduced towards reading certain parts of this phantom textbook (read: prompting an LLM to generate a proof or explore some problem) and sharing the resulting text with others, which of course anybody else could have found if they simply also knew the right point of the textbook.

To be blunt, this seems incredibly uninteresting to me. I enjoy learning mathematics, sure, but I just don't find much inherent meaning in reading a textbook or a paper. The meaning comes from the taking those ideas and applying them to my own problems, be it a direct proof of a conjecture or coming up with the right framework or tools for those conjectures. But, of course, in this future, those proofs and frameworks are already in the textbook. So what's the point? If someone cared about these answers in the first place, they probably could have found the right prompt to extract it from this phantom textbook anyways.

You could argue for there being work still like marginal improvements and applying the returned proof to other scenarios as happened in this case, but as above, what is really there to do if this is already in the phantom textbook somewhere and you just need to prompt better? The mathematicians in this case added to the exposition of the proof, but why wouldn't the phantom textbook already have good enough exposition in the first place?

I think my complete dismissal of the value of things like extending the proofs from an LLM or improving exposition is too strong -- there is value in both of them, and likely will always be -- but it would still represent a sharp change in what a mathematician does that I don't think I am excited for. I also don't think this phantom textbook is contained even in the weights of whatever internal model was used here just yet (especially since as some of the mathematicians in the article pointed out, a disproof here did not need to build any new grand theories), but it really does seem to me it eventually will be, and I can't help but find the crawl towards that point somewhat discouraging.

I believe D. A. Jimenez and C. Lin, "Dynamic branch prediction with perceptrons" is the paper which introduced the idea. It's been significantly refined since and I'm not too familiar with modern improvements, but B. Grayson et al., "Evolution of the Samsung Exynos CPU Microarchitecture" has a section on the branch predictor design which would talk about/reference some of those modern improvements.

All you have done is contribute a wikipedia article which is the second google result if you search the title of the video. Another user made a comment referencing a textbook they used to learn this material as well as some extended comments of their own - this actually provides information unlike a bare wikipedia link presented with a dismissive attitude.

Why do you think that the 2024 Putnam programs that they used to test were in the training data?

Putnam solutions can be found multiple places online: https://kskedlaya.org/putnam-archive/, https://artofproblemsolving.com/community/c3249_putnam. These could have appeared in the training of the base LLM DeepSeek-V3.2-Exp or as problems in the training set - they do not give further detail on what problems they selected from AOPS and as the second link gives they are there.

By that logic I can slice open a sphere and call it a sheet

You can do this. If you remove a point (or a line, or really any connected component), you get a space which is the same as the plane. What happens if you remove two distinct points? You end up with with a very thick circle. Three points? It starts to get harder to visualize, but you end up with two circles joined at a point. As you remove more points you will get more circles joined together. From a mathematical perspective, these spaces are very different. If we start to allow gluing arbitrary points in the sphere together it gets even worse, and you can get some pretty wild spaces.

The point of surgery is that by requiring this gluing in of these spheres along the boundary of the space we cut out, the resulting spaces are not as wild - or at least are easier to handle than if we do any operation. To give an example, one might have some space and we want to determine if it has property A. The problem is our space has some property B which makes it difficult to determine property A directly. But by performing surgery in a specific way, we can produce a new space which has property A if and only if the original space did, and importantly, no longer has property B.

For property As that mathematicians care about, surgery often does a good job of preserving the property. In contrast things like just cutting and gluing points together without care will typically change property A, so it does not help as much.

Likewise I wonder why we need to import a sphere rather than just pinch the ends of the tube shut and say it's now a sphere.

I am not an expect on surgery, but I think from a mathematical perspective, pinching the ends of the tube shut and gluing in a new sphere would be equivalent operations. This pinching operation would be formalized as a "quotient space", and you can formalize the sphere as a "quotient" space equivalent to the pinching.

In guideline 1v1 a lot of very high level games are decided by garbage RNG which I think is even less interesting than determining who is 0.1pps faster.

I have played a lot of (moderately high level) 1v1 tetris and I would have to disagree. In fact I often felt that the reverse is true - if I felt I died to garbage hole RNG, really that meant I was getting out pressured and would have lost eventually anyways. And while my playstyle was more aggressive, try to out speed opponent, I lost my fair share of games to people playing (much) slower but just incredibly efficient.

I agree there is an overall disappointing amount of interaction between players, though. Watching your opponents board and adjusting to it is hard and takes a while to build the skill to do. And a lot of the times you can just get away with it by playing faster and out pressuring and ignoring the other player.

Vector operations are widely used in common software. Java uses AVX512 for sorting. glibc uses SIMD instructions for string operations.

There have been efforts to reprove it with a more easily verified proof, but they've gone nowhere.

My understanding was that the so called "second generation proof" of the classification of finite simple groups led by Gorenstein, Lyons, Solomon has been progressing slowly but steadily, and only the quasithin case had a significant (but now fixed) hole. Are there other significant gaps that aren't as well known?

I am somewhat surprised issues of scripting and trading even exist in the registration system. Staggering enrollment times over a few days, with new waves every 20 minutes or so, mostly solves scripting issues since you are only competing with a fraction of the student body now. Giving courses waitlists once they are full, instead of allowing people to just directly register once a spot frees up, makes trading impossible since if you could trade you could have just registered for the course anyways.

I understand that the registration system is probably old and tied up in tons of just as old management software, but if the university really cared the solutions should be there.

You can just drop the course - pretty much every university (in the United States, at least) allows students to drop courses one or two weeks into the semester without any record (on say, a transcript). Otherwise students cannot possibly plan their semesters, since courses may not make material available until after the semester actually starts.

So if you are planning to sell the slots and it does not work out, you just drop the course, no harm to you.

When you get good enough at mathematics, you can tell if your proofs are correct or not without asking a TA to grade them for you.

This is simply not true - you can get a very good sense of when your argument is correct, yes. But having graded for (graduate, even!) courses, even advanced students make mistakes. It's not limited to students, either; tons of textbooks have significant errata, and its not as if no retraction in math has ever been issued.

These get corrected by talking with other people - if you have an LLM spew out this synthetic chain-of-reasoning data, you probably get at least some wrong proofs, and if you blindly try to scale with this I would expect it to collapse.

Even tying into a proof-checker seems non-trivial to me. If you work purely in the proof-checker, you never say anything wrong - but the presentations in proof checking language is very different from textual ones, so I would anticipate issues of the LLM leveraging knowledge from, say, textbooks in its proofs. You might also run into issues of the AI playing a game against the compiler rather than building understanding (you see elements of this in the proofs produced by AlphaProof). And if you start mixing natural language and proof checkers, you've just kicked the verification can up the road a bit, since you need some way of ensuring the natural language actually matches the statements being shown by the proof checker.

I don't think these are insurmountable challenges, but I also don't think its as simple as the "generate synthetic data and scale harder" approach the parent comment thinks. Perhaps I'm wrong - time will tell.

and finally find a path to the solution.

But how does the student, or in your case the LLM, know that it actually has the solution? For students, this is done by: a grader grading the homework, asking the professor at OH, working on problems with other peers who crosscheck as you go. I see no reason why this LLM produced synthetic data, without this correction factor, would not devolve into a mess of incorrect, maybe even not-even-wrong style "proofs". And then how can training on this yield anything?

All of which effort and edifice would collapse into the dumpster

Except it wouldn't, because the work towards the BSD would still be right and applicable to other problems. If someone proved the Riemann hypothesis false, all of our math (and there is a lot of it) surrounding the problem isn't immediately made worthless. The same is true for any mathematical conjecture.

I don't doubt the rest of your comment might have played a role, however.

If Computer Architecture were a really healthy field, classes would have to be taught from recently-published papers, because it was moving faster than a textbook could be published.

I really don't get this perspective. How can you possibly hope to understand "recently-published papers" without first understanding the basics of the field, which is what Hennessy and Patterson covers? Every subject has introductory textbooks from which introductory courses are taught, and then you can take more advanced courses that can, among other things, include material from recently-published papers. Are there even any fields where courses must be taught from recently-published papers?

On another note, it's not like no more computer architecture textbooks are made. Look at the Synthesis Lectures on Computer Architecture series.

Looking at how no samples other than the 3 samples in the "Long horizon memory" section have any camera movement which puts something offscreen and then back onscreen, it certainly seems that they are stretching the capabilities as far as they can in writing.

But how do you analyze the policies without doing science? Nothing in the above is sound to me.

"The proposed policies in the US all dramatically increase the cost of energy" - why? How do you even begin to conclude this without looking at some sort of (economic/scientific) analysis?

"only slightly slow the progression of warming" - again, how are you concluding this?

"we as a species have gotten really good as reducing deaths" - why should this trend continue? Why should it continue in the face of more extreme weather/climate change?

All I see are things you _think_ are true, and so to you your argument seems sound. But as the comment you replied to said, all I see is ignorant, sloppy science, since any meaningful analysis of these policies is by definition science. These cost/benefits you mention are not universal apparent truths.

Why does pretraining or not matter in the ISPD 2023 paper? The circuit_training repo, as noted in the rebuttal of the rebuttal by the ISPD 2023 paper authors, claims training from scratch is "comparable or better" than fine-tuning the pre-trained model. So no matter your opinion on the importance of the pretraining step, this result isn't replicable, at which point the ball is in Google's court to release code/checkpoints to show otherwise.

Do you have some examples of ones you found beyond what a human could straightforwardly figure out? I tried a bunch and they all seemed reasonable, so I would be interested in seeing - I didn't try all 400, for obvious reasons, so I don't doubt there are difficult ones.

I think regardless one of the reasons people are interested in it is that is a fairly simple logic puzzle - given some examples, extrapolate a pattern, execute the pattern - that humans achieve high accuracy on (a study linked on the website has ~84% accuracy for humans, some more recent study seems to put it closer to 75%). Yet ML approaches have yet to reach that level, in contrast to other problems ML has been applied to.

Given there is a large prize pool for the challenge, I would imagine actually training a model in the way you describe would already have been tried and is more difficult that it seems.

You might like the book "A History of Abstract Algebra" by Israel Kleiner - it goes over specifically the developments leading to the invention of the abstract group. The answer to your questions is that nobody really sat down and invented the group from the ether - its more accurate to say someone sat down and said "Hey, all these things we've been studying for the past 50 years are all the same thing if we think of it this way", and then the mathematical community eventually gets around to realizing its a useful abstraction (if it is one) as people build on it, or work more without it and eventually realize the abstraction would be helpful. For groups, this played out in how Cayley defined the abstract group in the 1850s, but it only started to gain more widespread usage in the 1870s. As for what they were doing, the main areas ways appeared around this time were through permutation groups (roots of polynomials), abelian groups (various number theoretic constructions/statements), and geometry (study geometry by studying groups of transformations, like isometries for Euclidean geometry).

I can guarantee you that way more men applied to Caltech than women did

Actually, my understanding was that women typically apply to higher education at higher rates than men. http://dx.doi.org/10.1016/j.econedurev.2004.09.008 has some data supporting this, but it is an older paper - has this changed in recent years, or is it different for Caltech specifically?

This also means that on average, a man on campus is more qualified to be there than a woman on campus

Given the article has a difference of 4 students (109 men to 113 women) I have a hard time believing there is a significant difference in abilities of the students. The small class size only further emphasizes this - when the applicant pool is around 13000 students and you are selecting the top 200 or so, you are selecting the high tail of the applicants, where differences in relative ability are marginal (unless you believe the ability distributions of men to women are vastly different.) Why can't it be the case that the top 500 applicants are all roughly equal in ability, and so no matter what distribution of men to women is picked you have low variance in the ability of the class?

Comparing common crawl to video makes no sense. Common crawl is text extracted from webpages. 424 terabytes of pure text contains exponentially more text than I will read in my entire life.

One application I like is the use of the Seifert-van Kampen theorem to prove that the fundamental group of the circle (S^1) is isomorphic to Z. While category theory is not strictly needed to prove this (you can compute pi_1(S^1) using R as a cover in a way that is purely topological, see Hatcher "Algebraic Topology"), if one states the Seifert-van Kampen theorem for groupoids (this uses category theory through the notion of a universal property/pushout) one can compute pi_1(S^1) largely algebraically just from the universal property - in fact you can go through the whole proof without mentioning a homotopy once (see tom Dieck "Algebraic Topology" section 2.7).

This might not meet your criterion exactly, as one can extract a more topological proof and relegate the category theory to a non-essential role, but this requires some more effort and is a harder proof. So I do think it still illustrates that the category theoretic approach does add something beyond just a common language.

The "No fix planned" is specifically for just the Ryzen 3000 desktop series. While obviously a fix would be better, given the age of this series as well as the need for ring 0 access to exploit the vulnerability, the actual impact from leaving it unfixed on those CPUs will probably be pretty limited.

I don't follow this argument, and there would still be issues with the computation anyways.

1) Pretend I want something written, and I want to minimize emissions. I can ask my AI or a freelancer. The total CO2 emissions of the entire industrial sector has nearly no relation to the emissions increase by asking the freelancer or not. Ergo, I should not count it against the freelancer in my decision making.

2) In the above scenario, there is always a person involved - me. In general, an AI producing writing must be producing it for someone, else it truly is a complete waste of energy. Why do the emissions from a person passively existing count when they are doing the writing, but not when querying?

3) If you do think this should be counted anyways, we are then missing emissions for the AI as the paper neglects to account for the emissions of the entire semiconductor industry/technology sector supporting these AI tools; it only computes training and inference emissions. The production of the GPUs I run my AI on are certainly an unalieanable part of having an AI do some job.

The way this paper computes the emissions of a human seems very suspect.

For instance, the emission footprint of a US resident is approximately 15 metric tons CO2e per year [22], which translates to roughly 1.7 kg CO2e per hour. Assuming that a person’s emissions while writing are consistent with their overall annual impact, we estimate that the carbon footprint for a US resident producing a page of text (250 words) is approximately 1400 g CO2e.

Averaging this makes no sense. I would imagine driving a car is going to cause more emissions than typing on a laptop. And if we are comparing "emissions from AI writing text" to "emissions from humans writing text" we cannot be mixing the the latter with a much more emissions causing activity and still have a fair comparison.

But that's besides the point, since it seems that the number being used by the authors isn't even personal emissions -- looking at the source [22], the 15 metric tons CO2e per year is labeled as "Per capita CO₂ emissions; Carbon dioxide (CO₂) emissions from fossil fuels and industry. Land-use change is not included."

This isn't personal emissions! This is emissions from the entire industrial sector of the USA divided by population. No wonder why AI is supposedly "100-1000x" more efficient. Counting this against the human makes no sense since these emissions are completely unrelated to the writing task the person is doing, its simply the fact they are a person living in the world.

What exactly do you mean by non-trivial/modern standards? While certainly the largest and most complicated theorems are currently out of reach of proof verifiers, there isn't a shortage of usage of them to prove important/modern theorems (of course certain fields are much more developed/more amenable to verification than others).

* https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ discusses a few recent usages in recent papers and the author's grant to formalize Fermat's last theorem.

* The liquid tensor experiment (https://www.quantamagazine.org/lean-computer-program-confirm...)

* Feit-Thompson was formalized in 2012.

I do largely agree that formal correctness within mathematics is not as important as it may seem, though this doesn't mean formal verification of a proof is completely orthogonal to understanding it - you can't formally verify something without really understanding the proof in the first place.

Handling two different writes to memory is not really a concern - existing speculative/out of order processors already solve this issue by completing (perform architectural side effects) instructions in-order. So even if two writes are made, one in each branch, by the time the write is meant to be completed, the prior branch is resolved and we know which write is actually meant to be made and the bad one can be discarded.

Doubling the execution units also isn't strictly needed - you can use the existing out-of-order core to send two sets of instructions through the same functional units. There will be more contention for the resources, possibly causing stalls, but you don't need to fully double everything.

Things similar to this idea are already done in processors - simultaneous multithreading, early branch resolution, conditional instructions, are all ideas that have similar implementation difficulties. So the reason this specific idea is not done is more in line with your last two points rather than the first two.

Has this WSI chip been taped out/verified? I must admit I am somewhat skeptical of TBs of SRAM, even at wafer scale integration. What would the power efficiency/cooling look like?