I asked a question on MathOverflow.
mathoverflow.net/q/508812/1946 #MathOverflow
06.03.2026 03:53
👍 2
🔁 1
💬 0
📌 0
I asked a question on MathOverflow.
mathoverflow.net/q/508812/1946 #MathOverflow
There's the MetaRocq project to write a verified version of it (in Rocq itself), but it still doesn't have a proof for termination, because that's precisely the part where Rocq does shady things whose consistency and semantics are unclear, and unsurprisingly three of Claude's bugs are there.
It's OCaml code, not formally verified, “validated” by the traditional method of code review :)
There's a list of them here, I haven't looked at them myself: tristan.st/blog/in_sear...
Oh my god, LLMs are autonomously finding inconsistencies in Rocq…
rocq-prover.zulipchat.com#narrow/chann...
Humour très, très niche 🙂
Je crois bien que c'est correct. Remplace "need" par "may" ou "must" et ça te surprendra sans doute moins.
(To be extra clear, I also think that even if one doesn't consider HoTT suitable as a foundation, it remains a mathematically interesting and technically useful object worth studying.)
in HoTT, I'm definitely thinking about something being “true”, but I don't really want that something to be a very complicated statement about simplicial sets or some variety of cubical sets—so what is it? This is why HoTT has made me feel philosophical discomfort that anti-classical math hasn't.
If I want to translate it to set-level foundations, I have half a dozen models available, but unlike the beginning of the subject, when Voevodsky's simplicial set model was considered canonical, I feel that in the present state of research none of them stands out as such. So when I prove a theorem …
There are even things which I now tend to think about in HoTT because I find it more intuitive. Yet if I try to make more precise what I really have in mind, I'm kind of stuck (and to be clear, this is not in favor of univalent foundations!).
Still, I think the ontology of Russian constructivism is clear: if I want to translate a theorem to ZFC, I just interpret it in the effective topos.
But what is the ontology of HoTT? I am perfectly able to work in HoTT, by appealing (when needed) to pre-mathematical intuitions about spaces.
However you do totally have a point about constructive math — for this comparison I would mainly count anti-classical schools, e.g., Russian constructivism. Not sure why I didn't think of this, silly me (I edited).
I mean, if I prove some theorem in PM and you're working in ZFC, it's pretty straightforward for you to translate it to your setting. The two foundations have a least upper bound of sorts. PM and other set-level type theories don't force a “types-as-sets” ontology but they're compatible with it.
Why philosophers of mathematics should care about univalent foundations (homotopy type theory):
mathstodon.xyz/@jeanas/1161...
(@joeldavidhamkins.bsky.social)
… primitive element which is a linear (not just algebraic) combination of the roots, and moreover "most" linear combinations are primitive elements, so you search it under this form? But it's elegant and a bit magical that you manage to do this computation without the algebraic closure.
I think I'm starting to understand this better, though I'll need a little more time to digest it. As I understand it, your idea is that by the strengthening of the primitive element theorem that the standard proof shows, the subfield of the algebraic closure generated by the roots will have a …
Wait, you meant to use an explicit description of the conjugates of y in a rupture field k[y]/⟨P⟩? What is this description?
Sorry, I didn't get the very last part, what is the linear algebra you do?
To be sure I understand, the reason for the “Zariski-closed” bit is that g is not separable iff the resultant of g and g' vanishes?
Oh yes, I'm interested.
Thank you! At least the beginning was very helpful (and even without details it's helpful to know when a problem is hard, which is what the books always neglect to tell you…). I couldn't much follow the rest, you lost me at “infinitesimals” 😅
I see papers about sophisticated ways to compute splitting fields efficiently, but they're above my head. What's the naive brute force algorithm for this?
Expanding the LHS and using the simplification X^n = R(X) to write it in the basis 1, X, …, X^(n-1), I'm reduced to finding if a variety in affine n-space over ℚ has a point. But that's Hilbert's 10th problem over the rationals, whose decidability is wide open 😵💫
Say k = ℚ. I know how to find roots in ℚ, using the rational root theorem, so I can factor P. But in the next step, I will need to find roots in a rupture field of ℚ, say roots of Q in ℚ[X]/⟨R⟩. So I look for a₀, …, a_(n-1) ∈ ℚ where n := deg(Q) such that Q(a₀ + a₁X + ⋯ + a_(n-1)X^(n-1)) = 0.
2. The standard construction of the splitting field of P seems to be: pick an non-linear irreducible factor of P, add a root α of it using a rupture field, rinse and repeat with P/(X-α) until it's split. Being algorithmically minded, I'm wondering how you actually do this computation.
No divisors of zero is enough to ensure inverses (every integral domain which is a finite-dimensional k-algebra is a field), but that's not a very simple condition either. (I do know about the primitive element theorem, but it doesn't really answer the question.)
1. To build a finite extension of k with basis (x₀, …, xₙ₋₁), I need to choose the coefficients that express xᵢxⱼ as a linear combination of x₀, …, xₙ₋₁ for 0 ≤ i, j < n. Is there a simple explicit description of how much freedom I have on this choice? Associativity of multiplication seems tricky.
