[proofplan]
We construct the isomorphism in both directions. A point derivation $D:A(X)\to k$ restricts to a functional on $\mathfrak m_p$, and the Leibniz rule forces it to vanish on $\mathfrak m_p^2$, so it descends to $\mathfrak m_p/\mathfrak m_p^2$. Conversely, a functional on $\mathfrak m_p/\mathfrak m_p^2$ defines a point derivation by applying it to the class of $f-f(p)1_{A(X)}$. The two constructions are then checked directly to be inverse $k$-linear maps.
[/proofplan]
[step:Send a point derivation to its induced functional on $\mathfrak m_p/\mathfrak m_p^2$]
Let $\operatorname{Der}_{k,p}(A(X),k)$ denote the $k$-[vector space](/page/Vector%20Space) of $k$-linear maps $D:A(X)\to k$ satisfying
\begin{align*}
D(fg)=f(p)D(g)+g(p)D(f)
\end{align*}
for all $f,g\in A(X)$.
Fix $D\in \operatorname{Der}_{k,p}(A(X),k)$. Since $1_{A(X)}(p)=1$, applying the defining identity to $1_{A(X)}\cdot 1_{A(X)}$ gives
\begin{align*}
D(1_{A(X)})=D(1_{A(X)})+D(1_{A(X)}).
\end{align*}
Subtracting $D(1_{A(X)})$ in the field $k$, we get $D(1_{A(X)})=0$. Hence $D(c1_{A(X)})=cD(1_{A(X)})=0$ for every $c\in k$.
If $a,b\in \mathfrak m_p$, then $a(p)=b(p)=0$, so the point-derivation identity gives
\begin{align*}
D(ab)=a(p)D(b)+b(p)D(a)=0.
\end{align*}
By $k$-linearity, $D$ vanishes on the ideal $\mathfrak m_p^2$, because $\mathfrak m_p^2$ consists of finite sums of products $ab$ with $a,b\in\mathfrak m_p$.
Therefore the restriction $D|_{\mathfrak m_p}:\mathfrak m_p\to k$ descends to a well-defined $k$-[linear map](/page/Linear%20Map)
\begin{align*}
\Phi(D):\mathfrak m_p/\mathfrak m_p^2\to k
\end{align*}
defined by
\begin{align*}
\Phi(D)(\overline a):=D(a),
\end{align*}
where $a\in\mathfrak m_p$ and $\overline a$ denotes the class of $a$ modulo $\mathfrak m_p^2$. This defines a $k$-linear map
\begin{align*}
\Phi:\operatorname{Der}_{k,p}(A(X),k)\to \operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k).
\end{align*}
[/step]
[step:Build a point derivation from a functional on $\mathfrak m_p/\mathfrak m_p^2$]
Let
\begin{align*}
\lambda:\mathfrak m_p/\mathfrak m_p^2\to k
\end{align*}
be a $k$-linear map. For $f\in A(X)$, the scalar $f(p)\in k$ is regarded as the constant function $f(p)1_{A(X)}\in A(X)$. Since
\begin{align*}
(f-f(p)1_{A(X)})(p)=0,
\end{align*}
we have $f-f(p)1_{A(X)}\in \mathfrak m_p$.
Define a map
\begin{align*}
D_\lambda:A(X)\to k
\end{align*}
by
\begin{align*}
D_\lambda(f):=\lambda(\overline{f-f(p)1_{A(X)}}),
\end{align*}
where the bar denotes the class in $\mathfrak m_p/\mathfrak m_p^2$. Because evaluation at $p$, subtraction of the corresponding constant function, the quotient map $\mathfrak m_p\to\mathfrak m_p/\mathfrak m_p^2$, and $\lambda$ are all $k$-linear, the map $D_\lambda$ is $k$-linear.
[guided]
Start with a functional
\begin{align*}
\lambda:\mathfrak m_p/\mathfrak m_p^2\to k.
\end{align*}
To turn $\lambda$ into a map on all of $A(X)$, we must first turn an arbitrary element $f\in A(X)$ into an element of $\mathfrak m_p$. The evaluation $f(p)\in k$ gives exactly the constant part of $f$ at the point $p$. We identify this scalar with the constant function $f(p)1_{A(X)}\in A(X)$ and define
\begin{align*}
f_0:=f-f(p)1_{A(X)}.
\end{align*}
Then
\begin{align*}
f_0(p)=f(p)-f(p)=0,
\end{align*}
so $f_0\in\mathfrak m_p$. Thus the class $\overline{f_0}\in\mathfrak m_p/\mathfrak m_p^2$ is a valid input for $\lambda$.
We therefore define
\begin{align*}
D_\lambda:A(X)\to k
\end{align*}
by
\begin{align*}
D_\lambda(f):=\lambda(\overline{f-f(p)1_{A(X)}}).
\end{align*}
This formula is $k$-linear in $f$: evaluation $f\mapsto f(p)$ is a $k$-linear map, the assignment $f\mapsto f-f(p)1_{A(X)}$ is $k$-linear from $A(X)$ to $\mathfrak m_p$, the quotient map $\mathfrak m_p\to\mathfrak m_p/\mathfrak m_p^2$ is $k$-linear, and $\lambda$ is $k$-linear by hypothesis. Hence $D_\lambda$ is a $k$-linear map from $A(X)$ to $k$.
[/guided]
[/step]
[step:Verify the Leibniz rule for the constructed map]
Let $f,g\in A(X)$. Define
\begin{align*}
f_0:=f-f(p)1_{A(X)}
\end{align*}
and
\begin{align*}
g_0:=g-g(p)1_{A(X)}.
\end{align*}
Then $f_0,g_0\in\mathfrak m_p$, and
\begin{align*}
f=f(p)1_{A(X)}+f_0
\end{align*}
and
\begin{align*}
g=g(p)1_{A(X)}+g_0.
\end{align*}
Multiplying these decompositions in the $k$-algebra $A(X)$ gives
\begin{align*}
fg-f(p)g(p)1_{A(X)}=f(p)g_0+g(p)f_0+f_0g_0.
\end{align*}
Since $f_0g_0\in\mathfrak m_p^2$, its class in $\mathfrak m_p/\mathfrak m_p^2$ is zero. Therefore
\begin{align*}
D_\lambda(fg)=\lambda(\overline{f(p)g_0+g(p)f_0}).
\end{align*}
Using $k$-linearity of $\lambda$, we obtain
\begin{align*}
D_\lambda(fg)=f(p)\lambda(\overline{g_0})+g(p)\lambda(\overline{f_0}).
\end{align*}
By the definition of $D_\lambda$, this is
\begin{align*}
D_\lambda(fg)=f(p)D_\lambda(g)+g(p)D_\lambda(f).
\end{align*}
Thus $D_\lambda\in\operatorname{Der}_{k,p}(A(X),k)$.
[/step]
[step:Check that the two constructions are inverse and $k$-linear]
Define
\begin{align*}
\Psi:\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k)\to \operatorname{Der}_{k,p}(A(X),k)
\end{align*}
by $\Psi(\lambda):=D_\lambda$. The construction of $D_\lambda$ is $k$-linear in $\lambda$, so $\Psi$ is a $k$-linear map.
Let $D\in\operatorname{Der}_{k,p}(A(X),k)$ and $f\in A(X)$. Since $D$ vanishes on constant functions, we have
\begin{align*}
(\Psi(\Phi(D)))(f)=\Phi(D)(\overline{f-f(p)1_{A(X)}})=D(f-f(p)1_{A(X)})=D(f).
\end{align*}
Hence $\Psi\circ\Phi$ is the identity on $\operatorname{Der}_{k,p}(A(X),k)$.
Conversely, let $\lambda\in\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k)$ and let $a\in\mathfrak m_p$. Since $a(p)=0$, we have
\begin{align*}
(\Phi(\Psi(\lambda)))(\overline a)=D_\lambda(a)=\lambda(\overline{a-a(p)1_{A(X)}})=\lambda(\overline a).
\end{align*}
Thus $\Phi\circ\Psi$ is the identity on $\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k)$.
Therefore $\Phi$ and $\Psi$ are inverse $k$-linear isomorphisms. Since
\begin{align*}
T_pX=\operatorname{Hom}_k(\mathfrak m_p/\mathfrak m_p^2,k),
\end{align*}
this proves that $T_pX$ is naturally isomorphic to the $k$-vector space of point derivations $A(X)\to k$ at $p$.
[/step]
