There are many ways to define Specht modules (see the various "avatars" in my notes, and there are more I plan to add). The Okounkov-Vershik one is one of the less natural, as it only works in characteristic $0$ to the best of my knowledge. But yes, it is isomorphic to the Specht module. This should be in the book that I cite as [CSScTo10] in the above-linked notes.

NB: Lang's Proposition VIII.5.4 (sic) is about single-root extensions, not their normal closures. And I'm not sure if any derivation can be extended to the normal closure, so I don't know whether this applies here.

Probably something with derivations ("all derivations vanish") instead of automorphisms ("all automorphisms fix"). There has been a recent (very technical) work by Brantner and Waldron on inseparable Galois theory: people.maths.ox.ac.uk/brantner/…

If we dropped the $i \neq j$ restriction, then $A_n$ would be the Kronecker product $\left(E_n - I_n\right) \otimes \left(E_n - I_n\right)$, where $E_n$ is the $n\times n$ all-ones matrix. With the restriction, it is a diagonal block of this Kronecker product. Does this help? I don't know.

See mathoverflow.net/questions/189222/… for the integral inequality. The discrete one might be a particular case, not sure (no time to check).

For question 1, the answer is not all commutative rings. See mathoverflow.net/questions/132174/… .

@hans: Thank you! Still only for positive-definite forms, as I feared, but good to have nevertheless.

@hans: Can Sage really check lattices for isometry? I don't see this option.

The rook monoid describes cells in the Bruhat decomposition of the matrix ring $\mathbb{C}^{n\times n}$. See Exercise 4.3.9 in arxiv.org/abs/1409.8356v7 , for example. (I also remember seeing more on this in a recent paper by Hugo Woerdeman, but I cannot find it at the moment.)

SageMath has functionality for (lazy) power series (see, e.g., this recent talk), though many people prefer to work with polynomials instead. You can define your own algebras by implementing recursive reduction algorithms, though I wouldn't necessarily call this easy. I don't think any methods for Gröbner-Shirshov bases have been implemented yet.

SageMath these days has become quite convenient (and between the cell server, the CoCalc cloud and WSL, it is really not hard to get working), but what kind of calculations do you want to do?

@მამუკაჯიბლაძე: The classical approach in Hazewinkel, Witt vectors (via the Dwork lemma) looks perfectly fine to me. Alternatively, use symmetric functions or power series to define big Witt vectors and then take a quotient.

Wow, this has to be the most complicated way of introducing the $p$-typical Witt vectors, and it's not for lack of competition!

Identifying tensors with multilinear forms on the rows of a matrix, this is math.stackexchange.com/questions/3256098/… or §6.22 of arxiv.org/abs/2008.09862v3 .