32 citations · 80 across the 9 of their papers we have counts for
14 papers
Proof Artifact Co-training for Theorem Proving with Language Models
Jesse Michael Han, Jason Rute, Yuhuai Wu +2
Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specia…
On the close interaction between algorithmic randomness and constructive/computable measure theory
Jason Rute
This is a survey of constructive and computable measure theory with an emphasis on the close connections with algorithmic randomness. We give a brief history of constructive measur…
On the computability of graphons
Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer +2
We investigate the relative computability of exchangeable binary relational data when presented in terms of the distribution of an invariant measure on graphs, or as a graphon in e…
Schnorr randomness for noncomputable measures
Jason Rute
This paper explores a novel definition of Schnorr randomness for noncomputable measures. We say is uniformly Schnorr -random if for all lower semicomputable…
Algorithmic randomness and Fourier analysis
Johanna Franklin, Timothy McNicholl, Jason Rute
Suppose . Carleson's Theorem states that the Fourier series of any function in converges almost everywhere. We show that the Schnorr random points are…
Energy randomness
Joseph S. Miller, Jason Rute
Energy randomness is a notion of partial randomness introduced by Diamondstone and Kjos-Hanssen to characterize the sequences that can be elements of a Martin-Löf random closed set…
When does randomness come from randomness?
Jason Rute
A result of Shen says that if is an almost-everywhere computable, measure-preserving transformation, and is Ma…
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer +19
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the…
Algorithmic randomness for Doob's martingale convergence theorem in continuous time
Bjørn Kjos-Hanssen, Paul Kim Long V. Nguyen, Jason Rute
We study Doob's martingale convergence theorem for computable continuous time martingales on Brownian motion, in the context of algorithmic randomness. A characterization of the cl…
Van Lambalgen's Theorem for uniformly relative Schnorr and computable randomness
Kenshi Miyabe, Jason Rute
We correct Miyabe's proof of van Lambalgen's Theorem for truth-table Schnorr randomness (which we will call uniformly relative Schnorr randomness). An immediate corollary is one di…
Computable randomness and betting for computable probability spaces
Jason Rute
Unlike Martin-Löf randomness and Schnorr randomness, computable randomness has not been defined, except for a few ad hoc cases, outside of Cantor space. This paper offers such a de…
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces
Jeremy Avigad, Jason Rute
Let B be a p-uniformly convex Banach space, with p >= 2. Let T be a linear operator on B, and let A_n x denote the ergodic average (1 / n) sum_{i< n} T^n x. We prove the following…
Metastable convergence theorems
Jeremy Avigad, Edward Dean, Jason Rute
The dominated convergence theorem implies that if (f_n) is a sequence of functions on a probability space taking values in the interval [0,1], and (f_n) converges pointwise a.e., t…
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem
Jeremy Avigad, Edward Dean, Jason Rute
We analyze the pointwise convergence of a sequence of computable elements of L^1(2^omega) in terms of algorithmic randomness. We consider two ways of expressing the dominated conve…