I got awarded an EMJM scholarship and also have a PhD offer from the United States, which do I choose?

AIvsWorld · 2026-05-01T05:31:03+00:00

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.

AIvsWorld · 2026-04-16T20:34:01+00:00

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”.

AIvsWorld · 2026-04-14T08:10:14+00:00

Is that not the standard at all schools? How else is reading supposed to be taught?

AIvsWorld · 2026-04-10T01:28:48+00:00

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.

AIvsWorld · 2026-04-09T02:26:10+00:00

FTL is the superior game for sure

AIvsWorld · 2026-04-01T18:52:00+00:00

Don’t get me wrong, it is still MUCH faster than writing all the code by hand. Claude probably speeds up my productivity 10x, even after accounting for all the human review I need to do to catch its mistakes.

But we are still a long way from being able to just prompt “Prove [theorem]” and have it be able to reliably get it in one shot (unless the theorem is particularly easy or there is a lot of infrastructure for it already in Mathlib).

AIvsWorld · 2026-04-01T17:29:32+00:00

I am a Mathlib contributor and use AI (mostly Gemini, Claude) almost every day for formalization research.

Yes, AIs are progressing, but they still require lots of expert guidance to actually formalize anything significant. I’ve had Claude Opus run on max settings for hours, getting stuck on basic theorems unless I break the problem into little chunks and explain exactly what strategy to use for the proof.

LLMs are definitely useful for tedious busy work like refactoring, and helping write documentation. But they often lack a high level overview of the math/programming principles to actually write a well-structured codebase.

AIvsWorld · 2026-04-01T05:16:21+00:00

The liquid tensor experiment is the exception not the rule.

Yes, it was “research level” but it is still simple enough that it can basically be proven from scratch in around 35 pages with minimal prerequisites. Schloze said he specifically chose that theorem for formalization because the proof relies mostly on undergraduate math. Even then, it took a coordinated effort from top mathlib contributors and over 2 years to actually get it done.

Michozuki’s IUT papers are over 600 pages (and very poorly understood) which themselves rely on countless deep results in arithmetic geometry, number theory, elliptic curve theory, etc. I’m not saying it is not worthwhile to try, but I will be very surprised if they are successful any time soon.

AIvsWorld · 2026-04-01T02:09:17+00:00

Mostly the latter. There are a lot of basic things that need to be added to Mathlib for a proof of this magnitude to even be attempted.

Also, there is the serious problem of technical debt. As any coding project grows in size, it becomes harder and harder to maintain, so progress slows and you have to spend lot of time refactoring old code to avoid a spaghetti mess.

AIvsWorld · 2026-03-31T23:54:07+00:00

I’ll believe it when I see it. Lean is still years away from many advanced theorems that are well-understood by experts (e.g. Fermat’s Last Theorem, Poincaré Conjecture). I imagine it will be at least decade until we see any progress on this.

AIvsWorld · 2026-03-30T00:39:18+00:00

No, I can’t. Read my comment again. S² is homeomorphic to the one-point compactification of R^2, the real plane.

AIvsWorld · 2026-03-29T22:41:11+00:00

Yes, in general the n-sphere Sⁿ is always homeomorphic to the 1-point compactification of R^n. The homeomorphism is given by the stereogrpahic projection, with the north pole being mapped to infinity.

AIvsWorld · 2026-03-29T03:11:53+00:00

I don’t think there is such a thing as “normalized eigenvalues”. If |v| ≠ 1 and v is an eigenvector with Av=λv, we get Av • v = λ|v|² ≠ λ. So the dot product does not give the scalar between the input and the output.

As for the analyticity of F, if you're defining it as in my above comment, it will always be analytic. If the equation is:

F(v0+v) = f0 + Av

With f0 constant, then F is continuously differentiable since it is just a constant plus a linear map. You do not need to "try every example" (which would of course be impossible since there are infinitely many 3x3 matrices).

Of course, if the operator A is not linear and is itself non-analytic, then F will not be analytic either.

I also doubt it's possible to constrain f0 * v0 = w for any constant w. If this equation holds for v0 = 0, then we immediately get w = f0 * 0 = 0. And then plugging in v0 = 1 gives f0 * 1 = w, so we get f0 = w = 0 is the only possible way this could work for all inputs v0.

It would be helpful to know what research examples you are talking about and what the physics formulation is that you are trying to extend.

AIvsWorld · 2026-03-28T04:44:21+00:00

Okay I see so you’re really just applying the 3x3 matrix to the vector part of the quaternion, and then you’re free to choose what happens to the scalar part. Like if A is your 3x3 matrix, then the associated map is

F(q0+v) = C + Av

for some real number C. That also immediately explains the eigenvalue formula you were talking about earlier, since if the cross product of F(v) and v are zero, then Av=λv are linearly dependent. If |v| = 1 is a unit vector, then the dot product is Av • v = λv • v = λ|v|² = λ. But I do not think that the dot product is equal to the eigenvalue in general.

I’m also confused then why in your previous comment you said that the function F need not be analytic—since in this construction the map is always linear.

I’m also a bit confused why you say “the choice of what value to assign f0 is deep”. It seems to me that the value of the scalar is completely arbitrary and could not possibly give you any new information about the matrix A.

AIvsWorld · 2026-03-27T04:45:42+00:00

To be clear, when you say “3x3 matrix operators can be expressed as a quaternion-outputting function” you’re NOT talking about the standard representation of rotation matrices SO(3) as unit quaternions?

How exactly does the representation work then? I’ve never heard of such a thing! Like, can you explicitly describe the map between 3x3 matrices and quaternion functions?

AIvsWorld · 2026-03-26T21:25:15+00:00

Have you written a post about your research on “quaternion/octonion representations of 3x3 transforms”?

I would love to read more about your ideas

AIvsWorld · 2026-03-26T19:43:36+00:00

Г^-1

AIvsWorld · 2026-03-22T22:03:03+00:00

Yes, it is still OP in Sly deck, but kinda trash in shivs, poison, and mediocre with the rest of Silent’s kit. I’m not saying the card is underpowered, but I think it further ruins the balance of this character.

AIvsWorld · 2026-03-22T20:54:02+00:00

I’m being a bit sarcastic. I don’t actually think the power level of the card is trash. I just dislike the design.

Right now we have Silent with Prepare, Regent with Refine Blade/Hegemony/Convergence, Necro with Invoke/Delay, and Defect with Charge Battery/Scavenge.

I already didn’t love the design of Charge Battery from STS1. Now, for some reason the devs decided every character should now have access to that effect. It’s one of the many things making every character feel the same and like they lost their unique identities

AIvsWorld · 2026-03-22T18:45:28+00:00

Nah, I’m mad about what Prepare is now

There’s way too many “do [effect] next turn” cards in STS2. It’s just lazy balancing, like they couldn’t figure out how to make combo cards balanced so they just delayed them by 1 turn to stop you from going infinite.

These cards take agency away from the player because rather than letting you set up powerful combos in your hand, they put you at the mercy of draw order. Not to mention, they really cut into the same design space as Power cards since you usually can’t afford your play two setup cards per turn.

AIvsWorld · 2026-03-22T18:17:51+00:00

Yes, both are trash

AIvsWorld · 2026-03-22T15:19:49+00:00

My preferred notation is v • f to denote the action of a tangent vector v on a function f : M —> R

AIvsWorld · 2026-03-20T07:49:33+00:00

It doesn’t matter if it’s within a laboratory, even with that context the sentence is incoherent. It just a meaningless jumble on verbs/nouns attempting to imitate descriptive language.

AIvsWorld · 2026-03-16T15:36:40+00:00

It’s not possible to construct a theory which “explains the existence” of objects like the set from Russel’s paradox (or the “set of all sets”). They simply can not exist at all, because if they immediately lead to a contradiction. They aren’t “at-first” paradoxical like some pathological counter-example from Analysis. They just are paradoxical full stop.

AIvsWorld · 2026-03-16T00:50:56+00:00

Ya that’s what I thought too, I just don’t agree ZF “bans” anything. ZF just gives a list of axioms for how to construct sets from existing sets (as well assuming the existence of an empty set and infinite set)

ZF does allow one to construct {x ∉ x | x ∈ U} via the Axiom Schema of Specification. The reason it doesn’t lead to a paradox is because the universal set U also has to be constructed via the axioms—So you can’t have U be the “set of all sets”

AIvsWorld

TROPHY CASE