Machine-verified model proves genetic code properties in lean
Reasoning about the Genetic Code in Lean
Logic in Computer Science
Summary
The genetic code uses several different DNA sequences to produce the same proteins, but it can be tricky to prove this precisely with computers. The authors built a detailed computer model of the genetic processes using Lean 4, a tool that checks every step mathematically. They showed how DNA transcripts make RNA and then proteins, proving important facts like how this process can produce the same protein from different DNA codes. This kind of work helps avoid errors in biology software by making sure the code matches the real biology exactly.
What this means in practice
- •For bioinformatics developers: Create biologically accurate software models that are mathematically verified to prevent errors in genetic data processing.
- •For computational biologists: Use machine-verified proofs to improve the reliability of simulations involving genetic replication and mutation processes.
Authors
Colin T. Jones, Tyler R. Josephson
Abstract
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.