arXiv subjects

John Mackey

Publications and source records attributed to John Mackey.

11 recordsLinked to original sources

arXiv2026

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.

math.CO↗

arXiv2026

Chat-Based Support Alone May Not Be Enough: Comparing Conversational and Embedded LLM Feedback for Mathematical Proof Learning

We evaluate GPTutor, an LLM-powered tutoring system for an undergraduate discrete mathematics course. It integrates two LLM-supported tools: a structured proof-review tool that provides embedded feedback on students' written proof attempts, and a chatbot for math questions. In a staggered-access study with 148 students, earlier access was associated with higher homework performance during the interval when only the experimental group could use the system, while we did not observe this performance increase transfer to exam scores. Usage logs show that students with lower self-efficacy and prior exam performance used both components more frequently. Session-level behavioral labels, produced by human coding and scaled using an automated classifier, characterize how students engaged with the chatbot (e.g., answer-seeking or help-seeking). In models controlling for prior performance and self-efficacy, higher chatbot usage and answer-seeking behavior were negatively associated with subsequent midterm performance, whereas proof-review usage showed no detectable independent association. Together, the findings suggest that chatbot-based support alone may not reliably support transfer to independent assessment of math proof-learning outcomes, whereas work-anchored, structured feedback appears less associated with reduced learning.

cs.HC↗

arXiv2025

Generative AI alone may not be enough: Evaluating AI Support for Learning Mathematical Proof

We evaluate the effectiveness of LLM-Tutor, a large language model (LLM)-powered tutoring system that combines an AI-based proof-review tutor for real-time feedback on proof-writing and a chatbot for mathematics-related queries. Our experiment, involving 148 students, demonstrated that the use of LLM-Tutor significantly improved homework performance compared to a control group without access to the system. However, its impact on exam performance and time spent on tasks was found to be insignificant. Mediation analysis revealed that students with lower self-efficacy tended to use the chatbot more frequently, which partially contributed to lower midterm scores. Furthermore, students with lower self-efficacy were more likely to engage frequently with the proof-review-AI-tutor, a usage pattern that positively contributed to higher final exam scores. Interviews with 19 students highlighted the accessibility of LLM-Tutor and its effectiveness in addressing learning needs, while also revealing limitations and concerns regarding potential over-reliance on the tool. Our results suggest that generative AI alone like chatbot may not suffice for comprehensive learning support, underscoring the need for iterative design improvements with learning sciences principles with generative AI educational tools like LLM-Tutor.

cs.HC↗

arXiv2024

Pentagon Minimization without Computation

Erd\H{o}s and Guy initiated a line of research studying $\mu_k(n)$, the minimum number of convex $k$-gons one can obtain by placing $n$ points in the plane without any three of them being collinear. Asymptotically, the limits $c_k := \lim_{n\to \infty} \mu_k(n)/\binom{n}{k}$ exist for all $k$, and are strictly positive due to the Erd\H{o}s-Szekeres theorem. This article focuses on the case $k=5$, where $c_5$ was known to be between $0.0608516$ and $0.0625$ (Goaoc et al., 2018; Subercaseaux et al., 2023). The lower bound was obtained through the Flag Algebra method of Razborov using semi-definite programming. In this article we prove a more modest lower bound of $\frac{5\sqrt{5}-11}{4} \approx 0.04508$ without any computation; we exploit``planar-point equations'' that count, in different ways, the number of convex pentagons (or other geometric objects) in a point placement. To derive our lower bound we combine such equations by viewing them from a statistical perspective, which we believe can be fruitful for other related problems.

math.CO↗

arXiv2023

Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane

We present a comprehensive demonstration of how automated reasoning can assist mathematical research, both in the discovery of conjectures and in their verification. Our focus is a discrete geometry problem: What is $\mu_{5}(n)$, the minimum number of convex pentagons induced by $n$ points in the plane? In the first stage toward tackling this problem, automated reasoning tools guide discovery and conjectures: we use SAT-based tools to find abstract configurations of points that would induce few pentagons. Afterward, we use Operations Research tools to find and visualize realizations of these configurations in the plane, if they exist. Mathematical thought and intuition are still vital parts of the process for turning the obtained visualizations into general constructions. A surprisingly simple upper bound follows from our constructions: $\mu_{5}(n) \leq \binom{\lfloor n/2 \rfloor}{5} + \binom{\lceil n/2 \rceil}{5}$, and we conjecture it is optimal. In the second stage, we turn our focus to verifying this conjecture. Using MaxSAT, we confirm that $\mu_5(n)$ matches the conjectured values for $n \leq 16$, thereby improving both the existing lower and upper bounds for $n \in [12, 16]$. Our MaxSAT results rely on two mathematical theorems with pen-and-paper proofs, highlighting once again the rich interplay between automated and traditional mathematics.

cs.CG↗

arXiv2021

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.

physics.med-ph↗

arXiv2020

Tighter Bounds on Directed Ramsey Number R(7)

Tournaments are orientations of the complete graph, and the directed Ramsey number $R(k)$ is the minimum number of vertices a tournament must have to be guaranteed to contain a transitive subtournament of size $k$, which we denote by $TT_k$. We include a computer-assisted proof of a conjecture by Sanchez-Flores that all $TT_6$-free tournaments on 24 and 25 vertices are subtournaments of $ST_{27}$, the unique largest TT_6-free tournament. We also classify all $TT_6$-free tournaments on 23 vertices. We use these results, combined with assistance from SAT technology, to obtain the following improved bounds: $34 \leq R(7) \leq 47$.

math.CO↗

arXiv2019

The Resolution of Keller's Conjecture

We consider three graphs, $G_{7,3}$, $G_{7,4}$, and $G_{7,6}$, related to Keller's conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one of the graphs contains a clique of size $2^7 = 128$. We present an automated method to solve this conjecture by encoding the existence of such a clique as a propositional formula. We apply satisfiability solving combined with symmetry-breaking techniques to determine that no such clique exists. This result implies that every unit cube tiling of $\mathbb{R}^7$ contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of $\mathbb{R}^8$ exists (which we also verify), this completely resolves Keller's conjecture.

math.CO↗

arXiv2017

On the number of 5-cycles in a tournament

We find an exact formula for the number of directed 5-cycles in a tournament in terms of its edge score sequence. We use this formula to find both upper and lower bounds on the number of 5-cycles in any $n$-tournament. In particular, we show that the maximum number of 5-cycles is asymptotically equal to $\frac{3}{4}{n \choose 5}$, the expected number 5-cycles in a random tournament ($p=\frac{1}{2}$), with equality (up to order of magnitude) for almost all tournaments. Note that this means that almost all $n$-tournaments contain the maximum number of $5$-cycles.

math.CO↗

arXiv2014

Containment: A Variation of Cops and Robbers

We consider "Containment": a variation of the graph pursuit game of Cops and Robber in which cops move from edge to adjacent edge, the robber moves from vertex to adjacent vertex (but cannot move along an edge occupied by a cop), and the cops win by "containing" the robber---that is, by occupying all $\deg(v)$ of the edges incident with a vertex $v$ while the robber is at $v$. We develop bounds that relate the minimal number of cops, $\xi(G)$, required to contain a robber to the well-known "cop-number" $c(G)$ in the original game: in particular, $c(G) {\le} \xi(G) {\le} \gamma(G) \Delta(G)$. We note that $\xi(G) {\geq} \delta(G)$ for all graphs $G$, and analyze several families of graphs in which equality holds, as well as several in which the inequality is strict. We also give examples of graphs which require an unbounded number of cops in order to contain a robber, and note that there exist cubic graphs with $\xi(G) \geq \Omega(n^{1/6})$.

math.CO↗

arXiv2013

Graham's Number is Less Than 2^^^6

In [5] Graham and Rothschild consider a geometric Ramsey problem: finding the least n such that if all edges of the complete graph on the points {+1,-1}^n are 2-colored, there exist 4 coplanar points such that the 6 edges between them are monochromatic. They give an explicit upper bound: F(F(F(F(F(F(F(12))))))), where F(m) = 2^^(m)^^3, an extremely fast-growing function. By reducing the problem to a variant of the Hales-Jewett problem, we find an upper bound which is between F(4) and F(5).

math.CO↗