This lecture presents the Mathgraph Theorem Prover, focusing on its representation of propositions, graph organization, and solver architecture for first-order logic. The presentation includes demonstrations of the solver's capabilities and discusses the advantages and drawbacks of the chosen encoding.