@inproceedings{21720,
  abstract     = {We present an exact fully-dynamic minimum cut algorithm that runs in 𝑛𝑜⁡(1) deterministic update time when the minimum cut size is at most 2Θ⁡(log3/4−𝑐⁡𝑛) for any 𝑐 >0, improving on the previous algorithm of Jin, Sun, and Thorup (SODA 2024) whose minimum cut size limit is (log⁡𝑛)𝑜⁡(1). Combined with graph sparsification, we obtain the first (1 +𝜖)-approximate fully-dynamic minimum cut algorithm on weighted graphs, for any 𝜖 ≥2−Θ⁡(log3/4−𝑐⁡𝑛), in 𝑛𝑜⁡(1) randomized update time.
Our main technical contribution is a deterministic local minimum cut algorithm, which replaces the randomized LocalKCut procedure from El-Hayek, Henzinger, and Li (SODA 2025).},
  author       = {El-Hayek, Antoine and Henzinger, Monika H and Li, Jason},
  booktitle    = {Proceedings of the Annual ACM SIAM Symposium on Discrete Algorithms},
  issn         = {1557-9468},
  location     = {Vancouver, Canada},
  pages        = {613--663},
  publisher    = {Society for Industrial and Applied Mathematics},
  title        = {{Deterministic and exact fully-dynamic minimum cut of superpolylogarithmic size in subpolynomial time}},
  doi          = {10.1137/1.9781611978971.25},
  volume       = {2026},
  year         = {2026},
}

@article{22403,
  abstract     = {Linear phase‐contrast scanning transmission electron microscopy (STEM) techniques compatible with high‐throughput 4D‐STEM acquisition are widely used to enhance phase contrast in weakly scattering and beam‐sensitive materials. In these modalities, contrast transfer is often suppressed at low spatial frequencies, resulting in a characteristic contrast gap that limits contrast. Approaches that retain low‐frequency phase contrast exist but typically require substantially increased experimental complexity, restricting routine use. Dark‐field STEM imaging captures this missing low‐frequency information through electrons scattered outside the bright‐field disk, but discards a large fraction of the scattered signal and is therefore dose‐inefficient. Fused Full‐field STEM (FF‐STEM) is introduced as a 4D‐STEM imaging modality that overcomes these limitations by combining ptychographic phase reconstruction with tilt‐corrected dark‐field imaging within a single acquisition. Bright‐field data are used to estimate probe aberrations and reconstruct a high‐resolution phase image, while dark‐field data provide complementary low‐frequency contrast. The two channels are fused in Fourier space using Wiener‐band weighting based on the spectral signal‐to‐noise ratio, yielding transfer‐gap‐free images with high contrast. FF‐STEM preserves the upsampling and depth‐sectioning capabilities of ptychography, adds robust low‐frequency contrast characteristic of dark‐field imaging, and enables dose‐efficient, near–real‐time reconstruction.},
  author       = {You, Shengbo and Varnavides, Georgios and Khavnekar, Sagar and Palatkin, Nikita and Shao, Sihan and Wu, Mingjian and Stroppa, Daniel and Chernikova, Darya and Zhu, Baixu and Egoavil, Ricardo and Vespucci, Stefano and Krishnan, Dileep and Ye, Xingchen and Schur, Florian KM and Spiecker, Erdmann and Pelz, Philipp},
  issn         = {2198-3844},
  journal      = {Advanced Science},
  publisher    = {Wiley},
  title        = {{Gap‐free information transfer in 4D‐STEM via fusion of complementary scattering channels}},
  doi          = {10.1002/advs.76620},
  year         = {2026},
}

@article{20986,
  abstract     = {During complex vocal interactions, different features of acoustic stimuli are integrated to produce appropriate vocal responses,1 such as copying sounds during vocal matching behavior in some animals.2,3,4,5,6,7,8,9,10,11,12 However, little is known about the interplay and possible trade-offs between the different temporal and spectral acoustic features during these vocal exchanges.2,13,14 Nightingales can flexibly match the pitch of their tonal “whistle songs” in real time during counter-singing duels.15,16 Here, we show that the syllable duration of whistle playbacks could alter the song responses of wild nightingales, causing their whistle duration distribution to shift toward the presented stimulus duration. When exposed to whistle playbacks featuring unnatural combinations of pitch and duration, nightingales demonstrate a flexible trade-off between pitch matching and temporal imitation, yet they are constrained by their vocal repertoire. They selectively adapted their vocal responses to approximate these novel stimuli, aligning them with their natural whistle repertoire. We developed a computational model of nightingale whistle-matching behavior that revealed a hierarchical organization of acoustic feature production. During whistle matching, the feature integration process is constrained by the duration of syllables, and pitch matching follows within this temporal framework, forcing a trade-off between the two features. Our findings reveal a complex interplay between the spectral and temporal domains that shapes song-matching behavior.},
  author       = {Calderon Garcia, Juan Sebastian and Costalunga, Giacomo and Vogels, Tim P and Vallentin, Daniela},
  issn         = {1879-0445},
  journal      = {Current Biology},
  number       = {3},
  pages        = {791--798.e6},
  publisher    = {Elsevier},
  title        = {{Interplay between syllable duration and pitch during whistle matching in wild nightingales}},
  doi          = {10.1016/j.cub.2025.12.025},
  volume       = {36},
  year         = {2026},
}

@article{21006,
  abstract     = {Modern experimental methods in programmable self-assembly make it possible to precisely design particle concentrations, shapes and interactions. However, more physical insight is needed before we can take full advantage of this vast design space to assemble nanostructures with complex form and function. Here we show how a substantial part of this design space can be quickly and comprehensively understood by identifying a class of thermodynamic constraints that act on it. These thermodynamic constraints form a high-dimensional convex polyhedron that determines which nanostructures can be assembled at high equilibrium yield and reveals limitations that govern the coexistence of structures. We validate our predictions through detailed, quantitative assembly experiments of nanoscale particles synthesized using DNA origami. Our results uncover physical relationships underpinning many-component programmable self-assembly in equilibrium and form the basis for robust inverse design, applicable to various systems from biological protein complexes to synthetic nanomachines.},
  author       = {Hübl, Maximilian and Videbæk, Thomas E. and Hayakawa, Daichi and Rogers, W. Benjamin and Goodrich, Carl Peter},
  issn         = {1745-2481},
  journal      = {Nature Physics},
  pages        = {294--301},
  publisher    = {Springer Nature},
  title        = {{A polyhedral structure controls programmable self-assembly}},
  doi          = {10.1038/s41567-025-03120-3},
  volume       = {22},
  year         = {2026},
}

@article{21295,
  abstract     = {Depending on the type of flow, the transition to turbulence can take one of two forms: either turbulence arises from a sequence of instabilities or from the spatial proliferation of transiently chaotic domains, a process analogous to directed percolation. The former scenario is commonly referred to as a supercritical transition and frequently encountered in flows destabilized by body forces, whereas the latter subcritical transition is common in shear flows. Both cases are inherently continuous in a sense that the transformation from ordered laminar to fully turbulent fluid motion is only accomplished gradually with flow speed. Here we show that these established transition types do not account for the more general setting of shear flows subject to body forces. The combination of the two continuous scenarios leads to the attenuation of spatial coupling; with increasing forcing amplitude, the transition becomes increasingly sharp and eventually discontinuous. We argue that the suppression of laminar–turbulent coexistence and the approach towards a discontinuous phase transition potentially apply to a broad range of situations including flows subject to, for example, buoyancy, centrifugal or electromagnetic forces.},
  author       = {Yang, Bowen and Zhuang, Yi and Yalniz, Gökhan and Vasudevan, Mukund and Marensi, Elena and Hof, Björn},
  issn         = {1745-2481},
  journal      = {Nature Physics},
  pages        = {424--429},
  publisher    = {Springer Nature},
  title        = {{Discontinuous transition to shear flow turbulence}},
  doi          = {10.1038/s41567-025-03166-3},
  volume       = {22},
  year         = {2026},
}

@article{21483,
  abstract     = {Embryogenesis in the model plant Arabidopsis thaliana provides a framework for understanding how cell polarity and patterning coordinate with hormonal signalling to establish the plant body plan. Following fertilisation, the zygote divides asymmetrically to generate apical and basal lineages, establishing the apical–basal axis that defines future shoot and root poles. Genetic and molecular analyses of classical mutants including gnom, monopteros (mp), bodenlos (bdl) and topless revealed that localised auxin biosynthesis, directional transport and downstream transcriptional responses are central to apical–basal axis establishment and organ initiation. The main components of this regulation are polarly localised PIN auxin transporters and downstream modules involving MONOPTEROS and WUSCHEL-RELATED HOMEOBOX transcription factors. Advances in microscopy have transformed the study of Arabidopsis embryogenesis: fluorescence-compatible clearing reagents and three-dimensional reconstructions now permit quantitative analyses of cell geometry, division orientation, and cytoskeletal dynamics. Live ovule imaging setups with confocal laser scanning and multiphoton microscopes enable real-time observation of embryo development, while laser-assisted cell ablation can be used to probe cell-to-cell communication and fate plasticity. Together, these methodological breakthroughs position Arabidopsis embryos as a prime model for dissecting the chemical and biophysical cues that shape plant development.},
  author       = {Babic, David and Zupunski, Milan and Friml, Jiří},
  issn         = {1469-8137},
  journal      = {New Phytologist},
  number       = {3},
  pages        = {1483--1491},
  publisher    = {Wiley},
  title        = {{Imaging and genetic toolbox to study Arabidopsis embryogenesis}},
  doi          = {10.1111/nph.71072},
  volume       = {250},
  year         = {2026},
}

@article{21486,
  abstract     = {Sex-chromosome systems are highly variable across animals, but how they transition from one to another is not well understood. Diptera have undergone multiple sex-chromosome turnovers and expansions while maintaining their general chromosomal content, which makes them an ideal clade to study such transitions. We analyzed more than 100 dipteran whole-genome assemblies and identified 4 new lineages that underwent sex-chromosome turnover (in addition to the 5 previously reported). We find that the majority of turnovers happened in the group Schizophora, which tend to have fewer genes on Muller element F (the chromosome homologous to the ancestral insect X chromosome) than lower dipterans, a factor previously hypothesized to facilitate turnover. Most derived X chromosomes have higher GC content than autosomes, consistent with a high prevalence of male achiasmy in Diptera. In addition, an excess of gene movement out of the X is detected for most of these new X chromosomes, and many of these moved genes have high testis expression in Drosophila, suggesting that out-of-X gene movement contributes to the long-term demasculinization of X chromosomes.},
  author       = {Layana Franco, Lorena Alexandra and Toups, Melissa A and Vicoso, Beatriz},
  issn         = {2056-3744},
  journal      = {Evolution Letters},
  number       = {3},
  publisher    = {Oxford University Press},
  title        = {{Causes and consequences of sex-chromosome turnovers in Diptera}},
  doi          = {10.1093/evlett/qrag003},
  volume       = {10},
  year         = {2026},
}

@phdthesis{21854,
  abstract     = {As neural-network-based models grow both in size and popularity, interest has grown in making the models smaller and more efficient to train. To that end, many methods have been proposed to prune models by reducing their number of nonzero parameters. Additionally, parameter-efficient fine-tuning, in which a much smaller number of parameters than the total contained in the model is updated during training, has become very popular, especially in the space of Large Language Models. At the same time, the increasingly routine deployment of machine learning in real-world applications has spurred a drive to make them more trustworthy - in the sense of, among other things, being unbiased, interpretable, and editable. In this thesis, we examine the interplay between efficiency and trustworthiness.

First, we analyze the effects of model pruning on bias in computer vision models, demonstrating that increased sparsity leads to greater bias, largely as a function of increased model uncertainty in marginal cases. Based on this observation, we propose several bias mitigation techniques. Then, we demonstrate that example-specific model pruning can improve model interpretation methods while improving pruning efficiency to make example-specific model pruning feasible in real time. Then, we investigate the effectiveness of parameter-efficient and data-efficient model personalization via fine-tuning, demonstrating that it is highly feasible with very small computational and data resources. Finally, we consider efficiency in editing model knowledge using a custom synthetic data framework, demonstrating that parameter-efficient, low-rank fine-tuning frequently outperforms full-rank fine-tuning, and, additionally, that restricting which model blocks are fine-tuned frequently improves results. Together, the results in this thesis provide new insights and techniques for combining trustworthiness and efficiency during neural network inference and training.

},
  author       = {Iofinova, Eugenia B},
  issn         = {2663-337X},
  pages        = {237},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{On the utility and effects of efficiency in artificial neural networks}},
  doi          = {10.15479/AT-ISTA-21854},
  year         = {2026},
}

@misc{21857,
  abstract     = {The availability of powerful open-source large language models (LLMs) opens exciting use cases, such as using personal data to fine-tune these models to imitate a user’s unique writing style. Two key requirements for this functionality are personalization–in the sense that the output should recognizably reflect the user’s own writing style—and privacy–users may justifiably be wary of uploading extremely personal data, such as their email archive, to a third-party service. In this paper, we demonstrate the feasibility of training and running such an assistant, which we call Panza, on commodity hardware, for the specific use case of email generation. Panza’s personalization features are based on a combination of parameter-efficient fine-tuning using a variant of the Reverse Instructions technique [1] and Retrieval-Augmented Generation (RAG) [2]. We demonstrate that this combination allows us to fine-tune an LLM to reflect a user’s writing style using limited data, while executing on extremely limited resources, e.g. on a free Google Colab instance. Our key methodological contribution is the first detailed study of evaluation metrics for this task, and
of how different choices of system components–the use of RAG and of different fine-tuning approaches–impact the system’s performance. Additionally, we demonstrate that very little data - under 100 email samples - are sufficient to create models that convincingly imitate humans, showcasing a previously unknown attack vector in language models. We are releasing the full Panza code as well as three new email datasets licensed for research use.},
  author       = {Nicolicioiu, Armand and Iofinova, Eugenia B and Jovanovic, Andrej and Kurtic, Eldar and Nikdan, Mahdi and Panferov, Andrei and Markov, Ilia and Shavit, Nir and Alistarh, Dan-Adrian},
  booktitle    = {Third Conference on Parsimony and Learning (Proceedings Track)},
  keywords     = {LLMs, PEFT, LoRA, personalization, efficient ML},
  location     = {Tübíngen, Germany},
  publisher    = {OpenReview},
  title        = {{Panza: Investigating the feasibility of fully-local personalized text generation}},
  year         = {2026},
}

@unpublished{21859,
  abstract     = {As artificial neural networks, and specifically large language models, have improved rapidly in capabilities and quality, they have increasingly been deployed in real-world applications, from customer service to Google search, despite the fact that they frequently make factually incorrect or undesirable statements. This trend has inspired practical and academic interest in model editing, that is, in adjusting the weights of the model to modify its likely outputs for queries relating to a specific fact or set of facts. This may be done either to amend a fact or set of facts, for instance, to fix a frequent error in the training data, or to suppress a fact or set of facts entirely, for instance, in case of dangerous knowledge. Multiple methods have been proposed to do such edits. However, at the same time, it has been shown that such model editing can be brittle and incomplete. Moreover the effectiveness of any model editing method necessarily depends on the data on which the model is trained, and, therefore, a good understanding of the interaction of the training data distribution and the way it is stored in the network is necessary and helpful to reliably perform model editing. However, working with large language models trained on real-world data does not allow us to understand this relationship or fully measure the effects of model editing. We therefore propose Behemoth, a fully synthetic data generation framework. To demonstrate the practical insights from the framework, we explore model editing in the context of simple tabular data, demonstrating surprising findings that, in some cases, echo real-world results, for instance, that in some cases restricting the update rank results in a more effective update.},
  author       = {Iofinova, Eugenia B and Alistarh, Dan-Adrian},
  booktitle    = {arXiv},
  title        = {{Behemoth: Benchmarking unlearning in LLMs using fully synthetic data}},
  doi          = {10.48550/arXiv.2601.23153},
  year         = {2026},
}

@phdthesis{21957,
  abstract     = {This thesis investigates algorithmic certification and approximation methods for degenerate semidefinite programs (SDPs) and the singular roots of polynomial systems. In the first part, we present a hybrid symbolic-numeric algorithm for certifying the feasibility of weakly feasible, degenerate SDPs. By reformulating linear matrix inequalities (LMIs) into a structured polynomial system via facial reduction and incidence varieties, we guarantee the existence of an isolated exact solution. This algebraic reduction enables the certification of maximum-rank numerical approximations using methods from algebraic geometry.

In the second part, we address the severe ill-conditioning and loss of quadratic convergence that plague standard path-tracking methods near isolated singular roots. To overcome this, we propose tracking algorithms that achieve superlinear convergence without the computational bloat characteristic of classical deflation techniques. By modeling the solution path as a generalized fractional Puiseux series, our approach combines an explicitly derived algebraic predictor with a localized hyperplane desingularization phase during the corrector step. Furthermore, we introduce a continuous path-limit method and an extension of the geometric sequence rule to directly extract exact fractional exponents. This bypasses traditional heuristic trial-and-error methods and explicitly accommodates sparse series expansions. Numerical experiments confirm that our method significantly reduces the cumulative number of matrix inversions while achieving high-accuracy root approximations, even for heavily degenerate systems exhibiting higher coranks.},
  author       = {Zapata, Jeferson},
  isbn         = {978-3-99078-079-4},
  issn         = {2663-337X},
  pages        = {89},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Overcoming degeneracy and singularity: Techniques for semidefinite programs and homotopy continuation endgames}},
  doi          = {10.15479/AT-ISTA-21957},
  year         = {2026},
}

@phdthesis{21360,
  author       = {Riegler, Stefan},
  issn         = {2663-337X},
  pages        = {185},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Root system plasticity under nutrient limitation: Investigating hormonal and molecular drivers in Arabidopsis thaliana and Coffea  species}},
  doi          = {10.15479/AT-ISTA-21360},
  year         = {2026},
}

@misc{21363,
  abstract     = {The data contains information on coffee differential gene expression as well as co-expression and trait correlations in two separate experiments. First, contrasting nitrogen supply, second, intra- and interspecific grafting.},
  author       = {Riegler, Stefan},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Thesis Data for Root System Plasticity under Nutrient Limitation: Investigating Hormonal and Molecular Drivers in Arabidopsis thaliana and Coffea  species}},
  doi          = {10.15479/AT-ISTA-21363},
  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{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{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},
}

@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},
}

@phdthesis{22399,
  abstract     = {Gaining an understanding of how biological regulation evolves is a fundamental research 
question in both evolutionary biology and molecular genetics. In order to gain more insight 
into this topic, we focus on studying the simple gene regulatory system of the lac operon in 
E. coli. We show that simple population genetic models can shed light on evolution 
experiments and that this combined approach of modelling the experimental system gives 
insight to better understand the causes of evolutionary change in the experiment. We also 
study the natural diversity in the lac operon from 308 publicly available E. coli genomes that 
come from various host species and different regions of the world. Evidence that selection is 
generally maintaining the function of the lac operon across the sample regardless of host 
species is provided and we show that different protein coding genes in the operon are under 
different selective constraints on protein sequence preservation. A similar frameshift 
mutation found in experimental evolution studies is shown to be present in the sample we 
analyzed, indicating that selectively relevant variants in evolution experiments are also 
present in natural populations. We show that there is no simple phylogenetic relationship 
between host species, geographical location and the lac operon sequence. Finally, we argue 
that a combined approach of comparative genomics, experimental evolution and theoretical 
modelling contributes to a more complete understanding of molecular evolution. },
  author       = {Spasić, Aleksa},
  issn         = {2791-4585},
  pages        = {32},
  publisher    = {Institute of Science and Technology Austria},
  title        = {{Studying the evolutionary systems biology of the lac operon}},
  doi          = {10.15479/AT-ISTA-22399},
  year         = {2026},
}