Recent AI-Assisted Math Results
Papers and proofs using frontier models from companies like OpenAI, Anthropic, and Google.
/titles, abstracts + authors · this collection only
field
16 works · in the curator’s order
W_s7c8pz9c·v1published
Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs
Josh Alman, Virginia Vassilevska Williams
2h ago6 views
Fields: Computer Science; License: CC BY 4.0; Ancillary data: Proofs
W_yqt2gcbh·v1published
Linnik's constant is at most
Eric Naslund
21h ago5 views3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_64dxrxcs·v1published
An Exponent of 1.04273 for the Unit Distance Problem
Eric Naslund
22h ago6 views3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_gcjtkxyx·v1published
Continuity of solutions to abstract linear control systems
Frédéric Marbach
22h ago2 views3 downloads
Fields: Mathematics; License: CC BY-SA 4.0; Ancillary data: Proofs
W_7yhnzhrm·v1published
A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago2 views5 downloads
Fields: Computer Science; License: CC BY 4.0; Ancillary data: Proofs
W_d6vb6cpd·v1published
Finite Nash Equilibria and Dependent Mixed Strategies in Lean
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago1 view3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_5r2h2bs9·v1published
Prime-Generated Localization Descent for Unique Factorization in Lean
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
22h ago1 view3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_cpcvs4hw·v1published
An Executable Stallings Recognizer for Finite Generating Lists in Lean
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago1 view3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_4unwwyzv·v1published
Arrow and Gibbard Satterthwaite Theorems in Lean
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago1 view3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_2wpsx7jj·v1published
A Finite Coordinate Reduction for Approachability Loss in Lean
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago2 views3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_nex78vth·v1published
A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago1 view3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_9r35ktb7·v1published
Nash Bargaining Characterization in Lean
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago1 view3 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_z723dpvt·v1published
A Lean Formalization of Myerson-Satterthwaite Impossibility for Continuous Bilateral Trade
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago2 views3 downloads
Fields: Computer Science; License: CC BY 4.0; Ancillary data: Proofs
W_hurscggu·v1published
A Lean Formalization of the Classical Seifert van Kampen Groupoid Theorem
Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz
22h ago1 view2 downloads
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_mgx54xa8·v1published
Ordinal-definable families in Cohen, random, and collapse extensions
Elliot Glazer
22h ago1 view1 download
Fields: Mathematics; License: CC BY 4.0; Ancillary data: Proofs
W_gzgt89tf·v1published
for Bernoulli bond percolation on in all dimensions : a guide to the Lean formalization
Justin Leder
4d ago14 views3 downloads
Fields: Mathematics; License: Anthropic-public; Ancillary data: Proofs