This paper proposes extending the scope of digital humanities textual scholarship to the formal sciences — logic, mathematics, and computer science — and argues for the adoption of formal methods as a class of digital methods suited to this domain that have thus far been absent from DH practice.

The proposed application context is the study of concept and theory genesis in the formal sciences, a domain analogous to the history of concepts (Begriffsgeschichte) in historiography or motif research in literary studies. Just as certain motifs recur across literary traditions, particular concepts and theories pervade the history of mathematics. What distinguishes mathematics from literary culture is that its canonicity is constituted through formalization — and formalized texts are amenable to formal methods operating at the symbolic level that offer a precision unavailable to conventional DH approaches. Unlike statistical methods such as large language models, formal methods remain transparent and interpretable, and are free from the hallucination problem.

The paper argues for a two-component model of digital editions of mathematical texts, comprising a philological component — encoding the natural-language text according to standard editorial principles — and a formalist component that captures the conceptual and theoretical content in a fully formalized representation accessible to formal methods. TEI is proposed as the framework for the former; OMDoc (Kohlhase, 2006) for the latter. Existing digital editions of mathematical and scientific texts, such as the Newton Project and Bernoulli Euler Online, are shown to fall short of this standard by representing formulae only at the level of visual surface structure, rendering them unsuitable for formal analysis. While a fully formalized edition component remains a long-term goal requiring expertise in automated theorem proving beyond current DH capacities, the paper argues that this should not preclude first steps in this direction.