Post #2346200

2026-04-27 16:22 UTC

@tpfto@mathstodon.xyz @dpiponi@mathstodon.xyz Yes, exactly. Some expressions reveal real information even unevaluated. Many proofs contain a step that says “this yields the expression … which can be seen to be everywhere positive, therefore…”. Or for a concrete example, n³-6n²+11n-6 is always a multiple of 6 because it is equal to n(n-1)(n-2).

Replies (1)

@dpiponi@mathstodon.xyz 2026-04-27 16:45

@mjd@mathstodon.xyz @tpfto@mathstodon.xyz There's a two-stage process here. One is computing things when you don't yet have all of the information. But at the first stage these are literally the computations you might perform with pen and paper. At the second stage you reify those things. For example, an expression you might write when doing group theory becomes, itself, an element of the free group. It's an object that formally captures this idea of computing something with partial information. (I think you mentioned something about closures and monads the other day. This is closely connected. If you reify an expression written in group theory you get an element of a free group. But if you now write that down it looks identical to the original expression. This is the MM -> M of a monad.)

Open ##2346201