@article{21849, abstract = {The development of complex tissues relies on the precise assignment of cell identity. At the molecular scale, this process depends on the deposition of epigenetic modifications—such as methylation—that are regulated by complex biochemical networks and occur at specific regions on the DNA and chromatin. Here we show that despite the complexity of epigenetic regulation, dynamical scaling and self-similarity of DNA methylation marks emerge in embryonic development. Drawing on single-cell multi-omics experiments, super-resolution microscopy and statistical physics, we demonstrate that these phenomena originate in dynamical feedback between DNA methylation and the formation of nanoscale dynamic chromatin aggregates. These nanoscale processes lead to genome-wide increase in DNA methylation marks following a power law and self-similar correlation functions. Using this framework, we identify methylation patterns that precede gene expression changes in embryonic symmetry breaking. Our work identifies linear sequencing measurements as a laboratory to study mesoscopic biophysical processes in vivo.}, author = {Olmeda, Fabrizio and Lohoff, Tim and Kafetzopoulos, Ioannis and Clark, Stephen J. and Benson, Laura and Santos, Fatima and Krueger, Felix and Walker, Simon and Reik, Wolf and Rulands, Steffen}, issn = {1745-2481}, journal = {Nature Physics}, pages = {931--940}, publisher = {Springer Nature}, title = {{Scaling and self-similarity in the formation of the embryonic epigenome}}, doi = {10.1038/s41567-026-03263-x}, volume = {22}, year = {2026}, } @article{21883, abstract = {Three-dimensional (3D) printing has rapidly developed from a niche hobbyist activity into a widely accessible and indispensable technology across multiple scientific disciplines. Within microscopy, optical engineering laboratories and imaging core facilities, 3D printing enables creating customised solutions for sample holders, optical components and everyday laboratory tools that traditionally required specialised machining. By providing rapid prototyping, low-cost production and reproducibility, 3D printing facilitates innovation and efficiency in facility operations. This article provides a perspective on the possibilities, challenges, and practical aspects of implementing 3D printing within microscopy core facilities. Instead of providing technical review about 3D printing, we focus on service organisation, user engagement, resource management and community-driven repositories for design dissemination. Our aim is to share insights with those considering the implementation of 3D printing as a service for developing add-on components to ease the operation of different aspects of the machine-park driven services and those who are managing advanced instrumentation within research groups.}, author = {Goudarzi, Mohammad and Schuster, Maximilian and Milberger, Arthur and Gunkel, Manuel and Terjung, Stefan and Krens, Gabriel}, issn = {1365-2818}, journal = {Journal of Microscopy}, number = {3}, pages = {382--395}, publisher = {Wiley}, title = {{3D printing in core facilities – Low pain, high gain}}, doi = {10.1111/jmi.70106}, volume = {302}, year = {2026}, } @article{21872, abstract = {Magneto-optic Kerr effect (MOKE) is a powerful probe of broken time-reversal symmetry (T), typically used to study ferromagnets. While MOKE has been observed in some antiferromagnets (AFMs) with vanishing magnetization, it is often associated with structures whose symmetry is lower than basic collinear, bipartite order. In contrast, theory predicts a mechanism for MOKE intrinsic to all AFMs of A-type, i.e. layered AFMs in which ferromagnetic layers are antiferromagnetically aligned. Here we report the experimental confirmation of this mechanism in a bulk AFM. We achieve this by measuring the imaginary component of MOKE as a function of photon energy in MnBi2Te4, an A-type AFM where T is preserved in combination with a translation, and comparing the experimental results with model calculations. Our model suggests that observable MOKE should be expected in all collinear A-type AFMs with out-of-plane spin order, thus enabling optical detection of AFM domains and expanding the scope of MOKE to few-layer AFMs.}, author = {Sunko, Veronika and Ahsanullah, Salman and Jain, Vivek and Weber, Sophie and Kumaran, Sivaloganathan and Yan, Jiaqiang and Orenstein, Joseph and Ovchinnikov, Dmitry}, issn = {2041-1723}, journal = {Nature Communications}, publisher = {Springer Nature}, title = {{Magneto-optical Kerr effect in an A-type antiferromagnet}}, doi = {10.1038/s41467-026-72577-4}, volume = {17}, year = {2026}, } @article{21950, abstract = {One Health initiatives are modern paradigms for research and health care practices in various fields. Concrete definitions of the One Health framework, however, remain heterogeneous, leading to conceptual problems and uncertainties in the application of the framework. This article discusses several approaches to the One Health concept, and their associated consequences, with special focus on animal experimentation. The first issue addressed is how One Health should be defined, as well as what (and who) should be considered within a One Health approach. In order to shed further light on this, we explore the history of animals in biomedical science, highlighting historical milestones in the use of animal models, as well as the development and current state of ethical considerations in the field of animal experimentation. The second issue comes with the inclusion of animal experimentation per se as part of the One Health concept. Therefore, particular attention is paid to bioethical principles and the resulting problems that can arise when applying them to the One Health concept. Arguments such as the idea of inequality between humans and non-human animals, and the premise that all actions are done for the benefit of humans, are raised and then used to explore the question of whether the One Health concept is compatible with existing bioethical principles. Based on the bioethical principles of protecting the environment, the biodiversity and biosphere, this paper seeks an inclusive perspective of the One Health concept. Successful solutions will be based on this concept, which embraces all living beings. The authors conclude that a multispecies ethics approach could help create a more ethical ecosystem that is aligned with the wellbeing of all life on a shared planet.}, author = {Ulman, Yesim Isil and Kostomitsopoulos, Nikos and Camenzind, Samuel and Kitsara, Maria and Pavone, Ilja Richard and Schober, Sophie}, issn = {2632-3559}, journal = {Alternatives to Laboratory Animals}, number = {4}, pages = {226--235}, publisher = {SAGE Publications}, title = {{Emerging bioethical conflicts: One Health and animal experimentation}}, doi = {10.1177/02611929261453330}, volume = {54}, year = {2026}, } @article{21900, abstract = {Individually silencing 125 fruit fly genes reveals opposing fitness effects of mutations between females and males, as well as between germline and somatic tissues.}, author = {Ruzicka, Filip}, issn = {2397-334X}, journal = {Nature Ecology & Evolution}, pages = {1035--1036}, publisher = {Springer Nature}, title = {{Reverse genetics of sexual antagonism}}, doi = {10.1038/s41559-026-03036-y}, volume = {10}, 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}, } @article{21164, abstract = {Global emission inventories often fail to capture the complexities of vehicular pollution in regions with unique fuel mixes, such as Brazil’s extensive biofuel use, leading to significant uncertainties in atmospheric modeling. This study presents a century-long (1960–2100) bottom-up vehicular emission inventory for Brazil, leveraging locally derived emission factors. Our estimates reveal substantial discrepancies in magnitude, timing, and speciation of non-CO2 pollutants (CO, NMHC, PM2.5) compared to leading global inventories (EDGAR, CEDS, CAMS), highlighting critical inaccuracies in widely used data sets. More critically, future projections under Shared Socioeconomic Pathways (SSPs) uncover a novel positive feedback mechanism: rising temperatures significantly enhance vehicular evaporative nonmethane hydrocarbon (NMHC) emissions. This temperature-dependent increase and subsequent NMHC oxidation to CO2 suggest an overlooked pathway that could amplify climate warming and air pollution globally, particularly after a breakpoint around 2050 (p < 0.05). While historical emissions peaked in the 1990s–2000s, nonexhaust PM becomes increasingly important. Air quality simulations using our inventory in the MUSICA model show good regional PM2.5 agreement but highlight challenges in resolving local primary pollutant peaks. This comprehensive inventory provides crucial data for Brazil and uncovers globally relevant climate–chemistry interactions, urging a re-evaluation of regional specificities in global emission assessments.}, author = {Ibarra-Espinosa, Sergio and Dias de Freitas, Edmilson and Gaubert, Benjamin and Lichtig, Pablo and Ropkins, Karl and da Silva, Iara and Martins Pereira, Guilherme and Schuch, Daniel and Nascimento, Janaina and Hoinaski, Leonardo and Martins, Leila Droprinchinski and Gavidia-Calderón, Mario and Vara-Vela, Angel and Toledo de Almeida Albuquerque, Taciana and Ynoue, Rita Yuri and Diez, Sebastian and Mera, Zamir and Casallas Garcia, Alejandro and Vallejo, Fidel and Diaz, Valeria and Pedruzzi, Rizzieri and Abrutzky, Rosana and Franco, Marco A. and Huneeus, Nicolas and Jorquera, Hector and Belalcázar-Cerón, Luis Carlos and Rojas, Néstor Y. and de Fatima Andrade, Maria and Emmons, Louisa and Brasseur, Guy}, issn = {1520-5851}, journal = {Environmental Science & Technology}, number = {6}, publisher = {American Chemical Society}, title = {{A century of vehicular emissions in Brazil: Unveiling the impacts of unique fuel mix on air quality}}, doi = {10.1021/acs.est.5c08400}, volume = {60}, year = {2026}, } @article{20971, abstract = {Mountain glaciers are among the natural systems most vulnerable to climate change. However, their interactions with the atmosphere are complex and not fully understood. These interactions can trigger rapid adjustments and climate feedbacks that either amplify or attenuate atmospheric signals, influencing both glacier response and large-scale atmospheric circulation. Observing this functional coupling in nature is challenging because the key processes occur over a wide range of spatial and temporal scales. However, recent advances in observational techniques and modeling have provided new insights into these interactions. In this review, we summarize the current state of knowledge on glacier-atmosphere interactions in high-mountain regions at different scales, and highlight recent advances in observational and numerical modeling. We also highlight important knowledge gaps and outline future research directions to improve the prediction of glacier change in a warming world.}, author = {Sauter, T. and Brock, B. W. and Collier, E. and Goger, B. and Groos, A. R. and Haualand, K. F. and Mott, R. and Nicholson, L. and Prinz, R. and Shaw, Thomas and Stiperski, I. and Georgi, A. and Haugeneder, M. and Mandal, A. and Reynolds, D. and Saigger, M. and Sicart, J. E. and Voordendag, A.}, issn = {1944-9208}, journal = {Reviews of Geophysics}, number = {1}, publisher = {Wiley}, title = {{Glacier-atmosphere interactions and feedbacks in high-mountain regions - A review}}, doi = {10.1029/2024RG000869}, volume = {64}, 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{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}, } @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}, }