@article{20935,
  abstract     = {In situ cryo-electron tomography (cryo-ET) has emerged as the method of choice to investigate the structures of biomolecules in their native context. However, challenges remain for the efficient production and sharing of large-scale cryo-ET datasets. Here, we combined cryogenic plasma-based focused ion beam (cryo-PFIB) milling with recent advances in cryo-ET acquisition and processing to generate a dataset of 1,829 annotated tomograms of the green alga Chlamydomonas reinhardtii, which we provide as a community resource to drive method development and inspire biological discovery. To assay data quality, we performed subtomogram averaging of both soluble and membrane-bound complexes ranging in size from >3 MDa to ∼200 kDa, including 80S ribosomes, Rubisco, nucleosomes, microtubules, clathrin, photosystem II, and mitochondrial ATP synthase. The majority of these density maps reached sub-nanometer resolution, demonstrating the potential of this C. reinhardtii dataset as well as the promise of modern cryo-ET workflows and open data sharing to empower visual proteomics.},
  author       = {Kelley, Ron and Khavnekar, Sagar and Righetto, Ricardo D. and Heebner, Jessica and Obr, Martin and Zhang, Xianjun and Chakraborty, Saikat and Tagiltsev, Grigory and Michael, Alicia and Van Dorst, Sofie and Waltz, Florent and Mccafferty, Caitlyn L. and Lamm, Lorenz and Zufferey, Simon and Van Der Stappen, Philippe and Van Den Hoek, Hugo and Wietrzynski, Wojciech and Harar, Pavol and Wan, William and Briggs, John A.G. and Plitzko, Jürgen M. and Engel, Benjamin D. and Kotecha, Abhay},
  issn         = {1097-4164},
  journal      = {Molecular Cell},
  number       = {1},
  pages        = {213--230.e7},
  publisher    = {Elsevier},
  title        = {{Toward community-driven visual proteomics with large-scale cryo-electron tomography of Chlamydomonas reinhardtii}},
  doi          = {10.1016/j.molcel.2025.11.029},
  volume       = {86},
  year         = {2026},
}

@article{20858,
  abstract     = {Targeted antigen delivery to immune cells, particularly dendritic cells, has emerged as a promising strategy to enhance therapeutic efficacy of vaccines, while minimizing adverse effects associated with conventional immunization. In this study, we use our previously described small glycomimetic molecule that is selectively recognized by the Langerhans cell (LC)-specific surface receptor Langerin and demonstrate specific delivery of protein antigens to these specialized dendritic cells. Our results show that Langerin-mediated antigen delivery significantly enhances the immune response in vivo, resulting in increased expansion and activation of antigen-specific T cells, compared to immunization with unmodified antigen. We demonstrate the feasibility of our LC-targeted platform for immune cell-specific immunization with protein antigen and underscore the potential of LCs as an access point for next-generation vaccines and immunotherapies.},
  author       = {Rica, Ramona and Klein, Klara and Johnson, Litty and Carta, Gabriele and Sarcevic, Mirza and Langer, Freyja and Rademacher, Christoph and Wawrzinek, Robert and Quattrone, Federica and Sparber, Florian},
  issn         = {1525-0024},
  journal      = {Molecular Therapy},
  number       = {1},
  pages        = {397--406},
  publisher    = {Elsevier},
  title        = {{Langerhans cell-targeted protein delivery enhances antigen-specific cellular immune response}},
  doi          = {10.1016/j.ymthe.2025.10.008},
  volume       = {34},
  year         = {2026},
}

@article{20537,
  abstract     = {In this personal account, I describe the work performed in my research group on the development of methods that harness heterogeneous photocatalysts for light-mediated nickel-catalyzed cross-couplings. This includes catalytic systems using carbon nitride materials, dye-sensitized TiO₂, covalent organic frameworks (COFs), and conjugated polymers. The rationale behind the selection of materials and how their use led to the identification of catalyst deactivation, structure–activity relationships, and future opportunities is discussed.},
  author       = {Pieber, Bartholomäus},
  issn         = {1437-2096},
  journal      = {Synlett},
  number       = {1},
  pages        = {43--54},
  publisher    = {Georg Thieme Verlag},
  title        = {{Photochemical cross-couplings using semiconducting materials}},
  doi          = {10.1055/a-2690-9269},
  volume       = {37},
  year         = {2026},
}

@article{21987,
  abstract     = {We introduce JODIE, a genetic joint modeling approach that estimates how DNA loci influence human traits by partitioning genetic effects into four components: direct effects (from a child’s alleles), indirect maternal and paternal effects (from parents’ alleles), and parent-of-origin (PofO) effects (dependent on parental transmission of alleles), while uniquely accounting for assortative mating. We analyze 30,000 child-mother-father trios from the Estonian Biobank and the Norwegian Mother, Father, and Child Cohort, focusing on height, body mass index, and childhood educational test scores. We find direct effects to be the largest contributor to trait variation, but combined, indirect parental and PofO effects are similarly substantial. We support our results by within-family genome-wide association testing and identify 276 independently associated DNA regions with a complex interplay between direct, indirect, and PofO effects. By joint modeling, we show that direct, indirect, and PofO effects collectively shape human phenotypic variation across loci genome-wide.},
  author       = {Krätschmer, Ilse and Hegemann, Laura and Hofmeister, Robin J. and Corfield, Elizabeth C. and Mahmoudi, Mahdi and Delaneau, Olivier and Andreassen, Ole A. and Campbell, Archie and Hayward, Caroline and Marioni, Riccardo E. and Ystrom, Eivind and Havdahl, Alexandra and Robinson, Matthew Richard},
  issn         = {2666-979X},
  journal      = {Cell Genomics},
  keywords     = {direct genetic effects, DGE, indirect genetic effects, IGE, parent-of-origin effects, phenotypic variation, assortative mating, within-family GWAS, MoBa, EstBB},
  number       = {7},
  publisher    = {Elsevier},
  title        = {{Separating direct, indirect, and parent-of-origin genetic effects in the human population}},
  doi          = {10.1016/j.xgen.2026.101277},
  volume       = {6},
  year         = {2026},
}

@phdthesis{22258,
  abstract     = {Uncovering the genetic architecture of complex traits and pinpointing causal molecular drivers require the ability to distinguish true signals from noise within massive, high-dimensional omics datasets. To extract meaningful biological insights from these datasets, such as identifying causal genetic variants and proteins, scalable and accurate inference methods are essential. To this end, this thesis develops novel Bayesian inference frameworks based on Vector Approximate Message Passing and demonstrates their effectiveness in the modeling of disease onset times and quantitative physical and clinical measures.

First, we introduce gVAMP, a Bayesian framework tailored for Genome-Wide Association Studies that enables the joint modeling of quantitative complex traits across millions of genetic variants. gVAMP demonstrates superior accuracy in variable selection and out-of-sample polygenic risk prediction compared to state-of-the-art approaches. We model human height using 17 million whole-genome sequence variants from the UK Biobank, incorporating a vast number of rare variants and revealing novel associations. gVAMP achieves a prediction accuracy of approximately 46% for human height, representing the highest reported performance for this trait to date. 

Second, we present vampW, a Bayesian framework for survival analysis applied to proteomic data. By effectively handling right-censoring and complex protein dependencies within the UK Biobank Pharma Proteomics Project dataset, vampW identifies 219 protein associations across 24 disease outcomes, the majority of which are not among the top marginal discoveries. We further adjust protein levels for exponential age effects, yielding 1,308 associations and highlighting the sensitivity of the analysis to the chosen age-correction methodology. Finally, vampW improves upon the variable selection capabilities of the commonly used (penalized) variants of the Cox proportional hazards model and delivers state-of-the-art out-of-sample prediction of disease onset times.

Collectively, these methods provide powerful tools for dissecting the genetic architecture of complex traits and the proteomic drivers of disease onset. Furthermore, by delivering accurate polygenic risk scores and precise predictions of onset times, this work advances the capabilities of personalized medicine and clinical risk stratification.},
  author       = {Depope, Al},
  issn         = {2663-337X},
  keywords     = {Approximate Message Passing, GWAS, Genomics, Proteomics, Survival modeling},
  pages        = {169},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{From sparse selection to risk prediction: Approximate message passing for proteomic survival models and large-scale genomics}},
  doi          = {10.15479/AT-ISTA-22258},
  year         = {2026},
}

@article{21488,
  abstract     = {Human height is a model for the genetic analysis of complex traits, and recent studies suggest the presence of thousands of common genetic variant associations and hundreds of low-frequency/rare variants. Here, we develop a new algorithmic paradigm based on approximate message passing (genomic vector approximate message passing [gVAMP]) for identifying DNA sequence variants associated with complex traits and common diseases in large-scale whole-genome sequencing (WGS) data. We show that gVAMP accurately localizes associations to variants with the correct frequency and position in the DNA, outperforming existing fine-mapping methods in selecting the appropriate genetic variants within WGS data. We then apply gVAMP to jointly model the relationship of tens of millions of WGS variants with human height in hundreds of thousands of UK Biobank individuals. We identify 59 rare variants and gene burden scores alongside many hundreds of DNA regions containing common variant associations and show that understanding the genetic basis of complex traits will require the joint analysis of hundreds of millions of variables measured on millions of people. The polygenic risk scores obtained from gVAMP have high accuracy (including a prediction accuracy of ∼46% for human height) and outperform current methods for downstream tasks such as mixed linear model association testing across 13 UK Biobank traits. In conclusion, gVAMP offers a scalable foundation for a wider range of analyses in WGS data.},
  author       = {Depope, Al and Bajzik, Jakub and Mondelli, Marco and Robinson, Matthew Richard},
  issn         = {2666-979X},
  journal      = {Cell Genomics},
  number       = {5},
  publisher    = {Elsevier},
  title        = {{Joint modeling of whole-genome sequencing data for human height via approximate message passing}},
  doi          = {10.1016/j.xgen.2026.101162},
  volume       = {6},
  year         = {2026},
}

@article{22267,
  abstract     = {Thermal pollution, whether local or driven by global warming, threatens biodiversity in part through its detrimental effects on reproduction. Non-coding small RNAs (sRNAs) are crucial for maintaining germline developmental robustness under heat stress. Remarkably, we uncovered that neuronal sRNAs regulate germ cells’ thermotolerance, affecting both spermatogenic and oogenic germlines in a cell-non-autonomous manner. Furthermore, we demonstrate that, in RNAi mutants, an oxygen-sensing neural circuit, modulated by neuropeptide signaling, antagonizes germline maintenance, likely reflecting the nematode’s innate association of reduced oxygen levels with food availability and reproductive permissive environments. Finally, we provide evidence that laboratory-domesticated alleles of oxygen-response genes encoding neuropeptide receptor NPR-1 and hexacoordinated globin GLB-5 compromise germline thermotolerance. Hence, our findings raise the possibility that sensory perception, independent of direct environmental change, modulates germline integrity, highlighting a novel mechanism by which neural circuits integrate environmental information to safeguard reproductive fitness in fluctuating environments.},
  author       = {Ewe, Chee Kiang and Achache, Hanna and Schön, Hanna and Kontorovich, Leonid and Teichman, Guy and Weiss, Shir and Mogilevskaya, Anna and Valenski, Myriam and Anava, Sarit and Bardapurkar, Rutwik and Gingold, Hila and Posner, Rachel and Antonova, Olga and De Bono, Mario and Tzur, Yonatan B. and Rechavi, Oded},
  issn         = {1879-0445},
  journal      = {Current Biology},
  number       = {14},
  pages        = {3566--3579.e5},
  publisher    = {Elsevier},
  title        = {{Neuronal RNAi and oxygen-sensing circuit shape germline resilience to heat stress}},
  doi          = {10.1016/j.cub.2026.06.016},
  volume       = {36},
  year         = {2026},
}

@article{21980,
  abstract     = {Despite significant progress in the field of molecular electronics over the last two decades, the quantitative prediction of metal-molecule-metal junction conductance remains a challenge. The standard computational framework combines density functional theory (DFT) with nonequilibrium Green’s functions (NEGF) using low-rung exchange-correlation functionals such as PBE, which overestimate the conductances. More advanced correction methods exist but require complex workflows and high computational cost, limiting their accessibility. Here, we introduce a physically motivated approach that approximates results obtained with high-rung functionals. Our method fits the PBE-calculated transmission to a Breit-Wigner form and subsequently refines the fit parameters using molecular orbital energies and metal densities of states computed for the isolated subsystems with high-rung functionals. This approach is applicable to a broad range of molecular junctions yielding conductance values in quantitative agreement with experiments. Our approach is simple, low-cost, and accurate, making it well-suited for routine and large-scale prediction of single-molecule junction conductance.},
  author       = {Gulyaev, Artem and Hazarika, Jyotisman and Liu, Zhen-Fei and Venkataraman, Latha},
  issn         = {1530-6992},
  journal      = {Nano Letters},
  number       = {22},
  pages        = {7429–7434},
  publisher    = {American Chemical Society},
  title        = {{A computationally efficient and accurate method for predicting conductance of single-molecule junctions}},
  doi          = {10.1021/acs.nanolett.6c01462},
  volume       = {26},
  year         = {2026},
}

@phdthesis{22017,
  author       = {Kleinhanns, Tobias},
  isbn         = {978-3-99078-081-7},
  issn         = {2663-337X},
  pages        = {59},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Unraveling the origin and evolution of defects to enable advanced thermoelectric performance}},
  doi          = {10.15479/AT-ISTA-22017},
  year         = {2026},
}

@article{21009,
  abstract     = {We demonstrate that periodically driven quantum rotors provide a promising and broadly applicable platform to implement multigap topological phases, where groups of bands can acquire topological invariants due to non-Abelian braiding of band degeneracies. By adiabatically varying the periodic kicks to the rotor we find nodal-line braiding, which causes sign flips of topological charges of band nodes and can prevent them from annihilating, indicated by nonzero values of the patch Euler class. In particular, we report on the emergence of an anomalous Dirac string phase arising in the strongly driven regime, a truly out-of-equilibrium phase of the quantum rotor. This phase emanates from braiding processes involving all (quasienergy) gaps and manifests itself with edge states at zero angular momentum. Our results reveal direct applications in state-of-the-art experiments of quantum rotors, such as linear molecules driven by periodic far-off-resonant laser pulses or artificial quantum rotors in optical lattices, whose extensive versatility offers precise modification and observation of novel non-Abelian topological properties.},
  author       = {Karle, Volker and Lemeshko, Mikhail and Bouhon, Adrien and Slager, Robert-Jan and Ünal, F. Nur},
  issn         = {2469-9934},
  journal      = {Physical Review A},
  number       = {1},
  publisher    = {American Physical Society},
  title        = {{Anomalous multigap topological phases in periodically driven quantum rotors}},
  doi          = {10.1103/db9d-9bns},
  volume       = {113},
  year         = {2026},
}

@article{21406,
  abstract     = {This preliminary study investigates the trace-element composition of ostracod shells (Ostracoda: Crustacea) as biogenic calcium carbonates in their role as environmental sentinels of pollution. Using high-resolution in-situ analysis, we compared two contrasting coastal systems: the highly urbanized seascape of metropolitan megacity Hong Kong (HKSAR) and the agriculturally dominated waters of rural retreat Jeju Island, Republic of Korea (ROK). The goal was to assess whether anthropogenic stress gradients affect trace element-to‑calcium ratios (E/Ca) in the carapaces of shallow-marine Neonesidea Maddocks, 1969 species. Hereby, the focus is laid on potential differences in the effects of extreme urbanization and extreme agriculturalization. We analyzed 12 trace elements commonly incorporated into ostracod shells using Inductively Coupled Plasma–Mass Spectrometry (ICP-MS). Only Mn/Ca, Mg/Ca, and Ni/Ca ratios showed strong correlations with specific seawater physicochemical parameters. Notably, Mn/Ca differed significantly between the two sites, seemingly driven mainly by variations in nitrite nitrogen levels. This suggests that Mn incorporation is sensitive to pollution source, urban versus agricultural, though species-specific uptake effects cannot be excluded. No significant differences in elemental uptake were found between adult and A-1 juvenile stages of Neonesidea mutsuensis Ishizaki, 1961 or Neonesidea elegans (Brady, 1969), supporting the use of both age groups in environmental reconstructions and increasing potential sample yields. While remaining empirical and exploratory, our tentative findings suggest that ostracod geochemistry holds promise for marine pollution monitoring and cautiously supports the application of ostracod Mn/Ca ratios to reconstruct anthropogenic, particularly nitrogen-related, impacts in nearshore environments using sediment core records.},
  author       = {Jöst, Anna B. and Rodriguez Moreno, Maximiliano J and Kim, Taihun and Baker, David M. and Yasuhara, Moriaki and Not, Christelle A. and Karanovic, Ivana},
  issn         = {1879-3363},
  journal      = {Marine Pollution Bulletin},
  number       = {6},
  publisher    = {Elsevier},
  title        = {{Ostracod shell chemistry as proxy for coastal marine conditions of a highly urbanized megacity (Hong Kong SAR) and an agro-centric oceanic province (Jeju Island, Republic of Korea) – a preliminary comparative analysis}},
  doi          = {10.1016/j.marpolbul.2026.119493},
  volume       = {227},
  year         = {2026},
}

@article{22608,
  abstract     = {For tissues to spread, they must deform while staying intact. How spreading tissues balance flexibility with integrity is not yet well understood. Here, we show that keratin intermediate filaments adapt tissue mechanical resilience to the stresses arising in epithelial tissues during spreading. By analyzing the expansion of the enveloping cell layer (EVL) over the yolk cell in zebrafish embryos in vivo, we find that keratin network maturation in EVL cells is promoted by stresses building up within the spreading tissue. Through genetic interference and tissue rheology experiments, complemented by a vertex model with mechanochemical feedback, we demonstrate that stress-induced keratin network maturation in the EVL increases tissue viscosity, to prevent tissue rupture. Further, keratins are required in the yolk cell for mechanosensitive actomyosin network contraction and flow, the forces pulling the EVL. These dual mechanosensitive functions of keratins enable a balance between pulling force production and EVL mechanical resilience, ensuring uniform and robust tissue spreading.},
  author       = {Naik, Suyash and Keta, Yann-Edwin and Pranjic-Ferscha, Kornelija and Hannezo, Edouard B and Henkes, Silke and Heisenberg, Carl-Philipp J},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{Keratins coordinate tissue spreading by balancing spreading forces with tissue material properties}},
  doi          = {10.1038/s41467-026-72366-z},
  volume       = {17},
  year         = {2026},
}

@article{22601,
  abstract     = {Kontaktelektrifizierung tritt allgegenwärtig in der Natur auf, doch die Identität der Ladungsträger bleibt in den meisten Fällen unklar, mit Elektronen, Ionen oder nanoskopischen Materialfragmenten als mögliche Kandidaten. Ein Material, bei dem die übertragene Spezies mehr gewiss erscheint, sind Ionomere, d. h. Polymere mit mobilen Ionen, deren Ladung durch fest gebundene Gegenladungen ausgeglichen wird. Wenn Ionomere mit einer neutralen Oberfläche in Kontakt kommen, lädt sich diese mit dem Vorzeichen der mobilen Ionen auf, was stark auf Ionentransfer hindeutet. Der zugrundeliegende Mechanismus sowie die bestimmenden Einflussfaktoren dieses Transfers sind jedoch bislang nur unzureichend verstanden. In der vorliegenden Arbeit zeigen wir, dass die Bindungsaffinität zwischen den mobilen Ionen und dem Ionomer den Ladungstransfer maßgeblich bestimmt. Wir untersuchen Ionomere mit gebundenen Anionen und Kationen und erzeugen mittels Ionenaustausch Proben mit einer Reihe unterschiedlicher übertragbarer Ionen. Für das anionische Ionomer beobachten wir eine starke Abhängigkeit von der Bindungsaffinität, wobei mobile Kationen mit der höchsten Affinität am wenigsten Ladung übertragen. Eine schwächere, aber trotzdem klare Abhängigkeit wurde für das kationische Ionomer gemessen, welches der freien Hydratationsenergie der mobilen Anionen folgt. Mithilfe von optischer Emissionsspektroskopie mit induktiv gekoppeltem Plasma (ICP‐OES) bestätigen wir den Transfer von mobilen Ionen auf die Oberfläche der Gegenprobe. Unsere Ergebnisse bestätigen die Ladungsträgeridentität und den Mechanismus des Ladungstransfers bei ionomerischen Materialien, was auch für das allgemeine Verständnis von Kontaktelektrifizierung von Bedeutung sein könnte.},
  author       = {Hoffman Jr, John R and Freunberger, Stefan Alexander and Waitukaitis, Scott R},
  issn         = {1521-3757},
  journal      = {Angewandte Chemie},
  publisher    = {Wiley},
  title        = {{Ionentransfer während der Ionomer Kontaktelektrifizierung: Bindungsaffinität steuert Aufladung}},
  doi          = {10.1002/ange.5487708},
  year         = {2026},
}

@article{22404,
  abstract     = {We consider a class of two-dimensional tight binding models displaying conical intersections of the Bloch bands at the Fermi level. The setting includes the case of generic transitions between quantum Hall phases. We consider the longitudinal conductivity, as given by Kubo formula, describing the variation of the current after introducing a space-homogeneous electric field, in an adiabatic way. We obtain an explicit expression for the longitudinal conductivity, completely determined by the number of conical intersections and by the shape of the cones. In particular, the formula reproduces the known quantized values found for graphene and for the critical Haldane model. Furthermore, we discuss the validity of Kubo formula in presence of conical intersections in the spectrum, starting from the time-dependent Schrödinger equation. For electric fields which are weak and slowly varying in space and in time, we prove the validity of linear response from quantum dynamics.},
  author       = {Marcelli, Giovanna and Pigozzi, Lorenzo and Porta, Marcello},
  issn         = {1573-0530},
  journal      = {Letters in Mathematical Physics},
  number       = {4},
  publisher    = {Springer Nature},
  title        = {{Longitudinal conductivity at integer quantum Hall transitions}},
  doi          = {10.1007/s11005-026-02087-3},
  volume       = {116},
  year         = {2026},
}

@article{22607,
  abstract     = {Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".
Code: https://github.com/madvorak/duality/tree/v3.2.0},
  author       = {Dvorak, Martin and Kolmogorov, Vladimir},
  issn         = {3117-4604},
  journal      = {Annals of Formalized Mathematics},
  keywords     = {Farkas lemma, linear programming, extended reals, calculus of inductive constructions},
  publisher    = {EPI Sciences},
  title        = {{Duality theory in linear optimization and its extensions -- formally verified}},
  doi          = {10.46298/afm.14253},
  volume       = {2},
  year         = {2026},
}

@article{22602,
  abstract     = {Contact electrification occurs ubiquitously in nature, but the identity of charge carriers in most situations remains uncertain, with electrons, ions, or nanoscopic material fragments as viable candidates. One material where the species transferred seems more certain is ionomers, i.e., polymers that contain mobile ions balanced by fixed counter‐charges. When ionomers touch a neutral surface, the latter becomes charged in the sign of the mobile ion, strongly suggesting ion transfer. However, the mechanism and governing factors of transfer remain poorly understood. Here, we demonstrate that binding affinity between mobile ion and ionomer controls charge transfer with ionomers. We use ionomers with fixed anions and cations and perform ion exchange to create samples with a series of transferrable ions. We observe a strong binding‐affinity dependence for the anionic ionomer, such that mobile cations with the highest affinity transfers the least charge. Weaker, yet clear dependence was measured for the cationic ionomer, which follows the hydration free energy of the mobile anion. Using inductively coupled plasma optical emission spectroscopy (ICP‐OES), we confirm transfer of the mobile ions to the counter sample's surface. Our results confirm the identify and mechanism of charge transfer with ionomeric materials, with potential implications for contact electrification more broadly.},
  author       = {Hoffman Jr, John R and Freunberger, Stefan Alexander and Waitukaitis, Scott R},
  issn         = {1521-3773},
  journal      = {Angewandte Chemie International Edition},
  publisher    = {Wiley},
  title        = {{Ion transfer during ionomer contact electrification: Binding affinity controls charging}},
  doi          = {10.1002/anie.5487708},
  year         = {2026},
}

@phdthesis{21393,
  abstract     = {This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS (i.e., Mathematics and Computer Science). The aim is to create code that is understandable, believable, useful, and elegant. The code should stand for itself as much as possible without a need for documentation; however, this text redundantly documents our code artifacts and provides additional context that isn’t present in the code. This thesis is written for readers who know Lean 4 but are not familiar with any of the topics presented. We manifest truth and beauty in three formalized areas of MathematiCS.

We formalize general grammars in Lean 4 and use grammars to show closure of the class of type-0 languages under four operations; union, reversal, concatenation, and the Kleene star.

Our second stop is the theory of optimization. Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take “infinite values”. Additionally, we develop the basics of the theory of optimization in terms of the framework called General-Valued Constraint Satisfaction Problems, and we prove that, if a Rational-Valued Constraint Satisfaction Problem template has symmetric fractional polymorphisms of all arities, then its basic LP relaxation is tight.

Our third stop is matroid theory. Seymour’s decomposition theorem is a hallmark result in matroid theory, presenting a structural characterization of the class of regular matroids. We aim to formally verify Seymour’s theorem in Lean 4. First, we build a library for working with totally unimodular matrices. We define binary matroids and their standard representations, and we prove that they form a matroid in the sense how Mathlib defines matroids. We define regular matroids to be matroids for which there exists a full representation rational matrix that is totally unimodular, and we prove that all regular matroids are binary. We define 1-sum, 2-sum, and 3 sum of binary matroids as specific ways to compose their standard representation matrices. We prove that the 1-sum, the 2-sum, and the 3-sum of regular matroids are a regular matroid, which concludes the composition direction of the Seymour’s theorem. The (more difficult) decomposition direction remains unproved.

In the pursuit of truth, we focus on identifying the trusted code in each project and presenting it faithfully. We emphasize the readability and believability of definitions rather than choosing definitions that are easier to work with. In search for beauty, we focus on the philosophical framework of Roger Scruton, who emphasizes that beauty is not a mere decoration but, most importantly, beauty is the means for shaping our place in the world and a source of redemption, where it can be viewed as a substitute for religion.},
  author       = {Dvorak, Martin},
  isbn         = {978-3-99078-074-9},
  issn         = {2663-337X},
  pages        = {160},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Pursuit of truth and beauty in Lean 4: Formally verified theory of grammars, optimization, matroids}},
  doi          = {10.15479/AT-ISTA-21393},
  year         = {2026},
}

@article{19860,
  abstract     = {An eight-partition of a finite set of points (respectively, of a continuous mass distribution) in R^3
 consists of three planes that divide the space into 8 octants, such that each open octant contains at most 1/8 of the points (respectively, of the mass). In 1966, Hadwiger showed that any mass distribution in R^3 admits an eight-partition; moreover, one can prescribe the normal direction of one of the three planes. The analogous result for finite point sets follows by a standard limit argument. We prove the following variant of this result: any mass distribution (or point set) in R^3 admits an eight-partition for which the intersection of two of the planes is a line with a prescribed direction. Moreover, we present an efficient algorithm for calculating an eight-partition of a set of n points in R^3 (with prescribed normal direction of one of the planes) in time O(n^7/3). A preliminary version of this work appeared in SoCG’24 (Aronov et al., 40th International Symposium on Computational Geometry, 2024).},
  author       = {Aronov, Boris and Basit, Abdul and Ramesh, Indu and Tasinato, Gianluca and Wagner, Uli},
  issn         = {1432-0444},
  journal      = {Discrete & Computational Geometry},
  pages        = {1331--1355},
  publisher    = {Springer Nature},
  title        = {{Eight-partitioning points in 3D, and efficiently too}},
  doi          = {10.1007/s00454-025-00739-0},
  volume       = {75},
  year         = {2026},
}

@article{22408,
  abstract     = {Solitons—localized wave packets that travel without spreading—play a central role in understanding transport and properties of nonlinear systems. In quantum many-body systems, however, such robust excitations are typically destroyed by thermalization. Here, we theoretically demonstrate the existence of solitonic excitations in high-energy states of Rydberg atom chains in the regime of strong nearest-neighbor Rydberg blockade. These localized wave packets propagate directionally atop a special class of reviving initial states related to quantum many-body scars and are capable of carrying energy. Exhibiting long coherence times, these states constitute a form of non-ergodic quantum dynamics and can be efficiently implemented on Rydberg atom simulators. In this work, in addition to a phenomenological description of solitons, we identify their counterpart in a classical nonlinear dynamical system, demonstrate their potential use in quantum information transfer, and conjecture their relevance for anomalous energy transport reported in numerical studies of Rydberg atom arrays.},
  author       = {Kerschbaumer, Aron and Desaules, Jean-Yves Marc and Ljubotina, Marko and Serbyn, Maksym},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{Quasi-solitons in Rydberg atom chains}},
  doi          = {10.1038/s41467-026-75598-1},
  year         = {2026},
}

@article{22101,
  abstract     = {Evolutionary biology examines how the genetic and phenotypic composition
of populations changes over time. An important goal is to determine the
fixation probability of a single advantageous mutant that arises in a homogeneous
population of N residents. Many real populations experience environmental
gradients that cause mutations to be beneficial in some spatial
regions but harmful in others. Here, we study the fixation probability of a
mutant placed on a simple one-dimensional spatial structure that experiences
such a gradient. The mutant’s fitness varies linearly from1 − s to 1 + s, whereas
the resident fitness is constant and equal to 1. The existing literature suggests
that such heterogeneity in the mutant’s fitness should lead to a decrease in its
fixation probability. However, in this work, we find that small, non-negligible
gradients (s < 1=√N) substantially increase the fixation probability,while larger
gradients (s > (log N)/√N) substantially decrease it.Moreover, we quantify the
strength of this phenomenon analytically and we precisely delimit the range of
the gradients for which it occurs. Our computer simulations closely match
those findings. Altogether, our results indicate that subjecting a simple
population structure to natural environmental conditions can produce strong
counterintuitive effects.},
  author       = {Svoboda, Jakub and Nemati, Hossein and Tkadlec, Josef and Kaveh, Kamran and Chatterjee, Krishnendu},
  issn         = {2041-1723},
  journal      = {Nature Communications},
  publisher    = {Springer Nature},
  title        = {{The effect of the fitness gradient on fixation probability}},
  doi          = {10.1038/s41467-026-71777-2},
  volume       = {17},
  year         = {2026},
}

