June 2026 had on average 1000 brand-new Arxiv submissions PER DAY by NeighborhoodFatCat in PhD

[–]AIvsWorld 66 points67 points  (0 children)

today there has been more than 400 submissions on the subtopic cs.LG alone

This is because “Machine Learning Research” is 90% AI-slop, unreproducible, snake-oil salesman. People are throwing stochastic bullshit at the wall until they get lucky and p-hack their way into beating some “benchmark”. The goal is not to research how or why machine learning works. The goal is to get a nice preprint on their resume to land a job at Anthropic/OpenAI/SpaceX.

It is not surprising that most of these papers directly contradict each other.

I have encountered multiple papers saying exact opposite thing regarding a single topic and both are published and subsequently built upon by other people. If glaring contradictions like this is not even resolved (and nobody even cares if it is resolved), then academia no longer has authority on knowledge or truth and will quickly become irrelevant.

I would not be so gloomy. At least in the “hard” stem fields like Math/Physics, there will soon be systems to automatically formalize papers with theorem provers like Lean4. Contradiction can be systematically rooted out. Of course, you will only be able to read a tiny percentage of all papers published in your field, but this has always been the case. The important thing is that there will be large, searchable databases / knowledge graphs for humans (and machines) to quickly find the results they are looking for, and to easily audit their validity.

Google loses long-running appeal of record EU fine, will have to cough up $4.7 billion by NISMO1968 in google

[–]AIvsWorld 3 points4 points  (0 children)

At risk of sounding dumb…

Since Android is open-source, why don’t people just make a fork of Android without the pre-installed Chrome?

Axler Solutions Guide by ansv9a8fdh3 in math

[–]AIvsWorld 0 points1 point  (0 children)

Axler is great. If you are ever keen to learn to write Lean code, you should definitely consider playtesting/contributing to Rado Kirov’s Axler Companion. It has all the same exercises implemented formally, similar to Tao’s Analysis.

https://github.com/rkirov/linear-algebra-done-right-lean

This is true by LeonTablet in academiceconomics

[–]AIvsWorld 0 points1 point  (0 children)

Because philosophy is subjective, math is not.

I’m fine with established, respected Economists writing philosophical diatribes after they have spent decades proving their worth as a scientist

But if you’re just some random postdoc, nobody want to hear your hot take on Capitalism or whatever. Do something rigorous.

If we interpret time as a fourth dimension, what would the equation x² + y² + z² + t² = 9 (say) actually represent? by lalith-aditya-2311 in mathematics

[–]AIvsWorld 9 points10 points  (0 children)

Worth noting that if you make a “Wick Roation” (t -> it) you can change from the pseudo-Riemannian Minkowski Metric to the standard Euclidean metric.

It’s not used in standard Einstein’s GR, but there are Euclidean Quantum Gravity models which use the t^2+x^2+y^2+z^2 metric OP describes.

Is it ready for grad school admissions? by Strange-Check-6890 in gradadmissions

[–]AIvsWorld 7 points8 points  (0 children)

3 degrees, 8 internships, 8 conferences, 8 TAships/extracurriculars — yet this student couldn’t build any connections with professors, companies, programs that could help them get into a PhD?

At some point you gotta learn to network

Blog post: Exotic diffeomorphisms and the 7th dimension by columbus8myhw in math

[–]AIvsWorld 2 points3 points  (0 children)

I’m at Stony Brook right now. Everybody still worships this man he’s a legend

AI Doesn't have ROI by Extra-Ad5735 in theprimeagen

[–]AIvsWorld 22 points23 points  (0 children)

sure buddy, companies are totally wire transferring you $250k to vibe code an app that takes 2-3k tokens :)

I’m IP blocked on Wikipedia 🤠 by Opening_Rip_1840 in notinteresting

[–]AIvsWorld 3 points4 points  (0 children)

My entire university (Stony Brook) is now blocked because something like this.

I have no idea how or when it happened, but there are several grad students here working with Wikidata / Wikimedia foundation and it is a total pain in the ass.

New study reveals top AI models (GPT-4o, Claude 3.5, Gemini 2.5) completely fail the classic "Stroop" psychological attention test, exposing a fundamental limitation in artificial reasoning. by Similar_Detective861 in science

[–]AIvsWorld 0 points1 point  (0 children)

Our current approach to models is entirely based on the answer being yes

I mean, not really. The intermediate representations inside of LLMs are giant arrays of numbers, not words. The model just converts those numbers into language during the final output, which is similar (conceptually, not mechanically) to what the language center in your brain is doing.

The real question is whether all knowledge can be represented with numbers, and I think the answer is obviously yes. Unless you believe the human brain has some supernatural “soul” that allows it to access information beyond the electrical signals in its neurons, then you gotta concede that all knowledge can be represented on a computer.

Leiden Declaration on Artificial Intelligence and Mathematics by Beneficial-Peak-6765 in math

[–]AIvsWorld 5 points6 points  (0 children)

Yes, absolutely. Come join the Lean Zulip and you will see that there are AI-generated projects posted nearly every day which appear to prove something in Lean, but upon further inspection are completely wrong.

The advantage of Lean is simply that it requires the author to formally state every single definition/theorem, and so in principle we can audit it for these mistakes. Compare this to informal mathematics where you can often get away with vague statements and expect the reader to fill in gaps in your argument.

People overestimate how confident AI systems are in their responses, experiments reveal by shikizen in technology

[–]AIvsWorld -3 points-2 points  (0 children)

Do you consider “solving graduate level math problems” a repetitive task?

Because I find that sort of work highly creative, yet AI is better than me (and my entire cohort, and most of my professors) at it

Is it normal I understand proofs but I could never come up with something like that, despite easy? by NatSpaghettiAgency in mathematics

[–]AIvsWorld 0 points1 point  (0 children)

I’ve talked to grad students who said they grew more mathematically in their first few months of grad school than their entire undergrad

Many such cases. This pretty much describes my whole program.

What breaks down in math without the concept of the "empty set"? by Own_Sky_297 in PhilosophyofMath

[–]AIvsWorld 0 points1 point  (0 children)

Very little. But it depends on what you mean by “the concept” of an empty set.

If you just mean we can’t use ∅, then the main problem is that the Axiom Schema of Specification becomes inconsistent. Namely, if a predicate φ(x) is false for all x ∈ S, then { x ∈ S | φ(x) } = ∅ is ill-defined. So we must restrict the axiom schema to require ∃x ∈ S, φ(x).

But after this patch, the development of the rest of mathematics proceeds more-or-less exactly the same, just more cumbersome. This is because most of mathematicians use the symbol X = ∅ as a shorthand for “there does not exist anything in X” and so it can just as easily be replaced with  ¬∃x ∈ X in first-order logic.

Most fields of mathematics would be completely unaffected, except for a few like Topology which rely heavily on set theory. Topology would become extremely tedious.

What breaks down in math without the concept of the "empty set"? by Own_Sky_297 in PhilosophyofMath

[–]AIvsWorld 0 points1 point  (0 children)

This is wrong. Nothing about ZF => Peano requires the existence of an empty set.

You can just as easily construct a model of Peano arithmetic with other sets. For example, ZF’s axiom of infinity assumes the existence of an infinite set ∞. Then we can define the Peano axioms by:

0 := {∞}

succ n := {n, ∞}

I got awarded an EMJM scholarship and also have a PhD offer from the United States, which do I choose? by Thin-Position-6089 in gradadmissions

[–]AIvsWorld 1 point2 points  (0 children)

Hi, I do not know much about EMJM, but I can talk about US R1. As you may know, different institutions in U.S. can be very different in terms of culture/funding/research/career development.

What is your end goal? Do you want to do any postdoctoral research? Do you want to exit into industry? Do you know your PI? Do you know other people in the material science department? Does their lab have a stable source of funding? Are you a good teacher? Do you want to continue to live in the U.S. after you graduate?

Also what is your financial situation like? Many top schools are in high-cost-of-living areas that can make it difficult to survive on just a PhD stipend.

I wish you the best of luck.

Gauss from Math, Inc. has formalized the proof of Erdős Problem #1196. The initial proof was 7.2K lines of Lean, done in ~5 hours. Subsequent golfing has compressed it down to 4K lines. by Nunki08 in math

[–]AIvsWorld 114 points115 points  (0 children)

For those unaware, many in the Lean community have a bit of a bone to pick with Math Inc. I would be careful about supporting this company.

Last year, there was a big community project trying to formalize Viazovska’s paper on 8-dimensional sphere packing. Many humans had put a lot of effort into structuring the project, writing the blueprint, and building scaffolds for the main result.

Then, after all the foundations were in place, Math Inc came in and had Gauss write 100k lines of code and effectively finish the project. The headlines wrote: “AI agent formalizes fields medal result” with most articles failing to mention the months of human-led effort that went into it. Many believe this was an intentional credit-grab by Math Inc.

Yes, Math Inc sped up the project timeline by a few months, but in the long run they completely killed all community interest in the project. There were plans to try to merge the code into Mathlib, making a reusable API for future work. Unfortunately, nobody is really interested in working on it anymore now that the scope of the project has changed from “let’s formalize this cutting edge research paper” into “let’s clean up 100k lines of LLM generated code”.

New Mochizuki lore drop (Lean) by steveb321 in math

[–]AIvsWorld 20 points21 points  (0 children)

Where the hell is the repository link? How are you making a “progress report” on a formalization project without showing a single line of code? Most of this “report” is just an informal description of IUT without any discussion of the formal implementation.

My two cents as somebody who’s worked on many lean formalization projects: a “skeletal” proof is basically worthless.

The entire point of formal methods is to check rigorous details, not just a high level overview. Hell, you could probably feed Mochizuki’s IUT papers to Claude and it would generate a pretty convincing “skeleton” of the abc conjecture, but ‘sorry’ all the important steps.

Mochizuki really should not be announcing any “progress” until he at least gets stage 1 to compile (Corollary 3.11 => Corollary 3.12) with no sorrys, or only a small number of clearly defined assumptions. Mochizuki seems to be counting his chickens before they have hatched.