Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery

Ramsey-good graphs are graphs that contain neither a clique of size $s$ nor an independent set of size $t$. We study doubly saturated Ramsey-good graphs, defined as Ramsey-good graphs in which the addition or removal of any edge necessarily creates an $s$-clique or a $t$-independent set. We present a method combining SAT solving with bespoke LLM-generated code to discover infinite families of such graphs, answering a question of Grinstead and Roberts from 1982. In addition, we use LLMs to generate and formalize correctness proofs in Lean. This case study highlights the potential of integrating automated reasoning, large language models, and formal verification to accelerate mathematical discovery. We argue that such tool-driven workflows will play an increasingly central role in experimental mathematics.

Three-Dimensional Virtual Histology in Unprocessed Resected Tissues with Photoacoustic Remote Sensing (PARS) Microscopy and Optical Coherence Tomography

Histological images are critical in the diagnosis and treatment of cancers. Unfortunately, the current method for capturing these microscopy images require resource intensive tissue preparation that delays diagnosis for many days to a few weeks. To streamline this process, clinicians are limited to assessing small macroscopically representative subsets of tissues. Here, we present a combined photoacoustic remote sensing (PARS) microscope and swept source optical coherence tomography (SS-OCT) system designed to circumvent these diagnostic limitations. The proposed multimodal microscope provides label-free three-dimensional depth resolved virtual histology visualizations, capturing nuclear and extranuclear tissue morphology directly on thick unprocessed specimens. The capabilities of the proposed method are demonstrated directly in unprocessed formalin fixed resected tissues. Here, we present the first images of nuclear contrast in resected human tissues, and the first 3-dimensional visualization of subsurface nuclear morphology in resected Rattus tissues, captured with a non-contact photoacoustic system. Moreover, we present the first co-registered OCT and PARS images enabling direct histological assessment of unprocessed tissues. This work represents a vital step towards the development of a real-time histological imaging modality to circumvent the limitations of current histopathology techniques.