Validation of RDF data is a key task for the Semantic Web and Knowledge Graphs. Shape Expressions (ShEx) is a popular language for RDF validation that has been presented with a formal semantics in several academic papers. We present a Lean 4 representation of ShEx based on two papers with machine-checked proofs of the main semantic results and of the validation algorithms presented in those papers, within a simplified model of RDF. The development of this encoding can help to extend the language with new features.