{"id":"arxiv:2610.36343","kind":"preprint","title":"Reasoning about the Genetic Code in Lean","authors":["Colin T. Jones","Tyler R. Josephson"],"author_count":2,"year":2026,"published":"2026-10-26","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2610.36343","nct_id":null,"source_url":"https://arxiv.org/abs/2610.36343","archive_url":"https://space-kitty.com/papers/arxiv:2610.36343","updated":"2026-10-26","pmid":null,"pmcid":null,"openalex_id":"W7224130498","pdf_url":"https://arxiv.org/pdf/2610.36343","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.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}