PaperlayerView exact revision on arXiv

Source-linked AI summary

Reasoning about the Genetic Code in Lean

Colin T. Jones, Tyler R. Josephson

arXiv:2610.36343v1cs.LO

TL;DR

Although genetic-code redundancy is well studied biologically, rigorous computational verification remains limited. The paper models central-dogma processes in Lean and proves properties including redundancy, injectivity, and length conservation. The authors also report that Lean helped prevent errors in definitions and proofs.

  • Problem

    Although genetic-code redundancy and related properties are well studied biologically, their formal verification in a rigorous logical and computational framework remains largely unexplored.

    Source: §1 · pp. 1–2

  • Method

    The authors formalize nucleic bases and amino acids as Lean inductive types and model transcription, translation, replication, reverse transcription, and mutation with functions.

    Source: §1 · p. 2, §3.2 · p. 3, §5 · p. 16

  • Results

    The formalization proves genetic-code redundancy, transcription length conservation, injectivity of DNA-to-RNA and reverse transcription, and length conservation and injectivity of DNA replication.

    Source: §5 · p. 16

  • Takeaways & Limitations

    Lean enabled the authors to prevent errors in their definitions and proofs, and they identify broader bioinformatics pipelines as possible targets for formal correctness guarantees.

    Source: §5 · p. 16

    The model omits RNA processing such as intron and exon splicing and does not yet account for biological differences between prokaryotes and eukaryotes or species-specific genetic-code variations.

    Source: §4.1.1 · p. 13

Abstract

from arXiv · show

The genetic code exhibits redundancy, meaning that multiple distinct nucleotide sequences can encode the same amino acid sequence, a property mathematically characterized as non-injectivity. While this phenomenon is well studied in molecular biology, its rigorous verification within a computational framework remains limited. In this work, we present a machine-verified model of the central dogma of molecular biology using the Lean 4 interactive theorem prover. We formalize nucleic acid bases and amino acids as inductive types and define transcription and translation as functions mapping DNA sequences to RNA and subsequently to polypeptides. Within this framework, we prove key properties of these biological processes, including the redundancy of the genetic code, injectivity of transcription, and the non-injectivity of translation. Additionally, we formalize auxiliary processes such as DNA replication and mutation, and verify properties such as length conservation under transcription and point mutations. Finally, we demonstrate how Lean 4 helps prevent semantic errors in our code, showing its effectiveness as a tool for advancing reliable, bug-free scientific computing, particularly within the life sciences.

1 Introduction

The paper frames the genetic code as a mathematical pattern suited to formalization, while noting that rigorous computational verification of its properties remains largely unexplored. It develops a Lean model to prove properties of the genetic code and related biological processes.

1 Introduction

  • Lean formalization targets errors that can undermine biological analyses, including off-by-one indexing errors that produced false positives in a retracted study.The paper presents formal methods as a way to prove such errors absent.Source: §1 · p. 1
  • The paper formalizes the standard genetic code in Lean and proves its redundancy, alongside properties of replication, reverse transcription, mutation, length conservation, and injectivity.Its stated goal is to bridge computational biology and formal methods with a verified codon-to-amino-acid mapping.Source: §1 · p. 2
  • The genetic code is described as a broadly shared biological pattern that can be studied mathematically, despite biology's complexity and variability.The passage characterizes biology as involving constraints, probabilities, and optimization principles.Source: §1 · p. 2
  • The central dogma describes information transfer from DNA through RNA to protein, with transcription and translation as its two stages.The paper also identifies DNA replication and reverse transcription as related pathways.Source: §1 · p. 2
  • Multiple codons can encode the same amino acid, while translation is non-injective and the other described processes are one-to-one.Leucine is specified by six codons; the passage also links redundancy to error minimization and evolutionary adaptation.Source: §1 · p. 2
  • Formal verification of genetic-code properties remains largely unexplored, while cited prior work includes HOL4 formalization of TP53-related pathways and a Coq neural-network model.The cited examples are Ahmad, Hasan, and Siddique and Bahrami et al..Source: §1 · p. 2

2 Methods

The methods passage identifies the Lean and supporting software versions used in the implementation.

2 Methods

  • The implementation used Lean 4 version 4.17.0-rc1, Mathlib4, and Visual Studio Code version 1.98.2.The source code is available in the ATOMS Lab Github.Source: §2 · p. 3

3 Defining the Genetic Code

The section formalizes the genetic code and related molecular processes in Lean, then proves properties including genetic-code redundancy, transcription injectivity, and length conservation. It also shows how formal definitions can abstract away important biological details.

3.1 Informal definitions

  • The informal framework describes information passing from DNA to RNA by transcription and from RNA to protein by translation, with codons mapping to amino acids.The section also identifies DNA replication and reverse transcription as related pathways.Source: §3.1 · p. 3

3.2 Formal definitions

  • The model defines DNA and RNA bases and amino acids as Lean inductive types, then uses functions to represent transcription and translation.Base checks distinguish DNA and RNA inputs; template transcription reverses the input sequence before mapping bases, while coding-strand transcription replaces thymine with uracil.Source: §3.2 · pp. 3, 4, 6, 7

3.3 Redundancy

  • Distinct coding-strand DNA codons AAA and GAA transcribe to UUU and UUC, which both translate to phenylalanine, demonstrating genetic-code redundancy.The section also reports transcription injectivity and length conservation under transcription.Source: §3.3 · pp. 8–9

3.4 Mutations

  • Point mutations replace one DNA base without changing strand length, and Lean verifies this length-conservation property.The section models mutations with list operations, but indices beyond the list length can produce unintended behavior.Source: §3.4 · pp. 9–10

3.5 DNA Replication

  • The DNA replication model maps each template base to its complement and proves length conservation and injectivity, while abstracting away biological machinery and strand-specific synthesis.The paper cautions that logical consistency of this definition does not establish faithful representation of DNA replication.Source: §3.5 · p. 10

3.6 Reverse Transcription

  • The paper defines reverse transcription as an inverse of template transcription, but notes that its complement-and-reverse mapping omits biological complexities such as enzyme-driven synthesis and possible errors.The resulting proofs of length conservation and injectivity therefore do not establish full biological fidelity.Source: §3.6 · pp. 10–11

4 Discussion

The discussion examines how biological edge cases constrain formal models and how Lean proofs can expose inconsistencies in their definitions. It highlights specific translation and RNA-processing mismatches, while noting that formal verification cannot eliminate semantic errors.

4.1 Challenges of Formal Biology

  • The discussion frames formalization as a defense against software errors, targeting syntax, runtime, and semantic problems during the editor stage before compilation.The cited table is described as covering errors in scientific computing software and typical interventions; its caption does not specify individual table entries.Source: Table 1 · p. 12, §4.1 · p. 12

4.1.1 The STOP Codon and Accuracy

  • The modeled translation treats STOP as an amino acid, may continue after STOP, and does not require translation to begin at AUG.The authors suggest splitting mRNA at STOP codons as a partial fix, while acknowledging that problems remain.Source: §4.1.1 · p. 13

4.1.2 Length Conservation

  • Eukaryotic intron splicing can change mRNA length and yield multiple transcripts from one DNA strand, challenging the model's transcription injectivity.Poly-A tails can also change mRNA length, but the discussion says they do not affect the modeled DNA-to-protein transformation because they add no coding information.Source: §4.1.2 · pp. 13–14

4.2 The Limits of Formalization

  • Lean can catch definition mistakes during proof-writing, but it cannot fully prevent semantic errors in models of biological processes.The discussion also notes that theorem provers mitigate syntactic and runtime errors, while remaining vulnerable to errors introduced when humans translate real-world concepts into formal definitions.Source: §4.1 · p. 12, §4.2 · p. 14
  • A proof attempt exposed a reverse-transcription direction error; more generally, failed proofs can reveal inconsistencies with the framework or biological expectations.The stated equivalence expectations apply only when there are no introns or additional mRNA processing steps.Source: §4.2 · p. 15

5 Conclusions and Outlook

The authors formalize central-dogma processes in Lean and prove redundancy and related properties. They make biological scope assumptions explicit and outline extensions to broader bioinformatics applications.

  • Lean models valid DNA bases, transcription by reversing the template and complementing bases, and translation by chunking RNA codons through a standard table into amino acids.Source: §5 · p. 16
  • A counterexample establishes genetic-code redundancy; proofs also cover transcription length, DNA/RNA injectivity and inverse relation, replication injectivity and length, and coding/template equivalence.Source: §5 · p. 16
  • The model's biological assumptions do not always hold, including for amino acids beyond the canonical 20 such as selenocysteine.Source: §5 · p. 16
  • Future extensions could add RNA splicing, translation initiation and termination, and gene-expression error correction; the authors identify any bioinformatics pipeline as a possible formalization target.Source: §5 · p. 16
  • Although the project was human-authored, the authors observe increasing AI competence at Lean; verification guarantees syntax correctness for AI-generated code, not semantic correctness.Source: §5 · p. 16
Loading 2610.36343v1…