The question involved here is natural and very classical, but I'm unsure what has been formally stated and proved in the literature. The only approach I know involves assembling facts that apparently weren't all known until the 1970s.

Start with a simple Lie algebra $\mathfrak{g}$ over $\mathbb{C}$, along with some Cartan subalgebra $\mathfrak{h}$ and the resulting weight lattice $X$ and root sublattice $X_r$ inside $\mathfrak{h}^*$ (Bourbaki's $P \supset Q$). Fix simple roots $\alpha_1, \dots, \alpha_\ell$ and corresponding fundamental dominant weights $\varpi_1, \dots, \varpi_\ell$. [The symbol \varpi gives an old version of the handwritten letter pi, for "poids".] Finite dimensional simple modules $L(\lambda)$ are then parametrized by dominant weights $\lambda$ with $L(0)$ the trivial module, while arbitrary finite dimensional modules are direct sums of these. Everything here just depends up to isomorphism on $\mathfrak{g}$, by standard conjugacy theorems.

Now the natural problem is: Find the smallest nontrivial (hence faithful) finite dimensional modules. By complete reducibility, it's enough to consider simple modules. A detailed answer requires the Killing-Cartan classification of simple Lie algebras, but there is a classification-free result:

All weights of $L(\lambda)$ lie in a single coset of $X_r$ in $X$, and these weights consist of Weyl group orbits of various dominant $\mu \leq \lambda$ in the standard ordering (possibly with multiplicity $>1$ if $\mu < \lambda$).

(1) Fix a coset not containing 0. Then there is a unique smallest nontrivial $L(\lambda)$ corresponding to a "minuscule" $\lambda$ (always one of the fundamental weights), with weights consisting of the Weyl group orbit of $\lambda$.

(2) Fix the coset containing 0. Then there is a unique smallest nontrivial $L(\lambda)$, whose weights consist of 0 together with the Weyl group orbit of $\lambda$. Here $\lambda^\vee$ is the highest root in the dual root system.

Is this written down and proved somewhere?

The history might also be interesting (or just messy). Once this result is in hand, it's not difficult to fill in the details for each simple Lie algebra, but much of that is found only in exercises of books by Bourbaki or me.

The question involved here is natural and very classical, but I'm unsure what has been formally stated and proved in the literature. The only approach I know involves assembling facts that apparently weren't all known until the 1970s.

Start with a simple Lie algebra $\mathfrak{g}$ over $\mathbb{C}$, along with some Cartan subalgebra $\mathfrak{h}$ and the resulting weight lattice $X$ and root sublattice $X_r$ inside $\mathfrak{h}^*$ (Bourbaki's $P \supset Q$). Fix simple roots $\alpha_1, \dots, \alpha_\ell$ and corresponding fundamental dominant weights $\varpi_1, \dots, \varpi_\ell$. [The symbol \varpi gives an old version of the handwritten letter pi, for "poids".] Finite dimensional simple modules $L(\lambda)$ are then parametrized by dominant weights $\lambda$ with $L(0)$ the trivial module, while arbitrary finite dimensional modules are direct sums of these. Everything here just depends up to isomorphism on $\mathfrak{g}$, by standard conjugacy theorems.

Now the natural problem is: Find the smallest nontrivial (hence faithful) finite dimensional modules. By complete reducibility, it's enough to consider simple modules. A detailed answer requires the Killing-Cartan classification of simple Lie algebras, but there is a classification-free result:

All weights of $L(\lambda)$ lie in a single coset of $X_r$ in $X$, and these weights consist of Weyl group orbits of various dominant $\mu \leq \lambda$ in the standard ordering (possibly with multiplicity $>1$ if $\mu < \lambda$).

(1) Fix a coset not containing 0. Then there is a unique smallest nontrivial $L(\lambda)$ corresponding to a "minuscule" $\lambda$ (always one of the fundamental weights), with weights consisting of the Weyl group orbit of $\lambda$.

(2) Fix the coset containing 0. Then there is a unique smallest nontrivial $L(\lambda)$, whose weights consist of 0 together with the Weyl group orbit of $\lambda$. Here $\lambda^\vee$ is the highest root in the dual root system.

Is this written down and proved somewhere?

The history might also be interesting (or just messy). Once this result is in hand, it's not difficult to fill in the details for each simple Lie algebra, but much of that is found only in exercises of books by Bourbaki or me.

REFERENCES: As I commented to Sasha Premet, I've only seen fragments of the story in earlier textbooks. There is a short note by H. Freudenthal in Proc. Amer. Math. Soc. 7 (1956), 175-176, concerning occurrence of the 0 weight; but this is superseded by later results. For general background and details on (1) and (2), I'll refer to [B1] = Bourbaki, Chap. 6 (1968), my book [H] = GTM 9 (1972), [B2] = Bourbaki, Chap. 8 (1975).

[B1]: $\S1$, Exer. 24, and $\S4$, Exer. 15.

[H]: Exer. 13.10 (just using root system axioms) and Prop. 21.3 (using basic representation theory), Exer. 21.3. Also Exer. 13.13 ("minimal nonzero" = "minuscule").

[B2]: $\S7.2$, $\S7.3$, and $\S7$, Exer. 22.