I solve mathematical problems and produce computer-assisted proofs. Using techniques from satisfiability solving and computer algebra, my work has enabled the solution of many hard combinatorial problems thousands of times faster than previously possible.

Currently, I am an assistant professor in the School of Computer Science at the University of Windsor. I completed my PhD in the Cheriton School of Computer Science at the University of Waterloo, and with Vijay Ganesh I lead the MathCheck project.

See my curriculum vitae or bio for a summary of my academic career and my research statement, publication list, or showcase for an overview of my research. If you are interested in working with me, the Algorithms & Mathematics group at Windsor is accepting applications for open research positions.

As of fall 2023, I am supervising or co-supervising 12 students. My group's webpage lists the students I'm working with or have worked with in the past.

# News

- June 2024: Yameen Ajani successfully defends his Master's thesis. He is now starting a developer position with Agriculture and Agri-Food Canada. Congratulations!
- June 2024: Four students I am supervising just had papers accepted: Zhengyu Li has a paper at IJCAI, Yameen Ajani has a paper at ISSAC, Aaron Barnoff has a paper at CIAA, and Nahiyan Alamgir has a paper at SC-Square.
- April 2024: Conor Duggan successfully presented his Master's project and graduated from Waterloo's Computational Mathematics program. He is now starting as a data analyst at AON Insurance. Congratulations!
- August 2023: Zhengyu Li successfully presented his Master's project and won computational math's best presentation award. He is now starting as a PhD student in computer science at Georgia Tech. Congratulations!
- June 2023: I gave an invited talk at the Dagstuhl seminar SAT Encodings and Beyond.
- June 2023: I was invited to speak at CanaDAM on our new bound on Kochen–Specker systems.
I have also organized a minisymposium on computer-assisted mathematics and will be presenting another talk (on the
`abc`conjecture) in the session on number theory. I also ended up giving an impromptu third talk on SAT solving when a speaker's flight was cancelled. - April 2023: I gave an invited talk at the Dagstuhl seminar Pushing the Limits of Computational Combinatorial Constructions.
- March 2023: We received 170 CPU years and 20 TB of storage from DRAC to further our work on Kochen–Specker systems.
- August 2022: Zhengyu Li and Daniel Dallaire both have papers appearing at the SC-square workshop this year. Both have graduated and are now pursuing Master's degrees: Zhengyu at the University of Waterloo and Daniel at the University of Ottawa. Congratulations!
- February 2022: I gave an invited tutorial at the Dagstuhl seminar New Perspectives in Symbolic Computation and Satisfiability Checking.
- January 2022: Noah Rubin successfully defends his Bachelor's thesis. His work resulted in a published paper at ICTAI and an extended abstract at AAAI. Congratulations, Noah!
- August 2021: I co-chaired (with James Davenport) the 2021 SC-square workshop held on August 19–20, 2021.
- May 2021: I presented the invited talk SAT Solvers for Combinatorics Problems at CanaDAM.
- January 2021: I joined the University of Windsor as an assistant professor (tenure-track).

# Publications

My work has been published in a number of notable venues including in the Communications of the ACM, in the Journal of Automated Reasoning, at the AAAI Conference on Artificial Intelligence 2018 (and 2019, 2021, 2022), at ISSAC 2024 (and 2018, 2011), at CASC 2016, at CASCON 2019, in the Journal of Experimental Mathematics, in the Journal of Symbolic Computation (twice), in the Annals of Mathematics and Artificial Intelligence, in IEEE Transactions of Information Theory, in Applicable Algebra in Engineering, Communication and Computing (receiving the 2020 best paper award), at ICTAI 2021, at IWOCA 2020, at IJCAI 2020, and appears in Maple in Mathematics Education and Research. Most of the articles are behind paywalls but preprints for each of my papers are available below if you do not have access through the publisher's site.

## Writings

Copies of my academic writings in reverse chronological order. The most recent are typically co-written with students that I am supervising and may be preprints in the process of being finalized. The oldest are reports written during my undergraduate studies that I have archived as a part of my lifelong commitment to improve my writing.

- June 27, 2024 SAT and Lattice Reduction for Integer Factorization [bib] conference
- June 23, 2024 SHA-256 Collision Attack with Programmatic SAT [errata] workshop
- June 21, 2024 Using Finite Automata to Compute the Base-
`b`Representation of the Golden Ratio and Other Quadratic Irrationals conference - May 28, 2024 A SAT+CAS Attack on the Minimum Kochen–Specker Problem conference
- January 24, 2024 AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems
- December 14, 2023 A SAT + Computer Algebra System Verification of the Ramsey Problem
`R`(3, 8) (student abstract) [bib] conference - December 14, 2023 A SAT Solver and Computer Algebra Attack on the Minimum Kochen–Specker Problem (student abstract) [bib] conference
- July 13, 2023 A Hybrid SAT and Lattice Reduction Approach for Integer Factorization [errata] workshop
- January 26, 2023 A New Lower Bound in the
`abc`Conjecture [bib] journal - November 16, 2022 A SAT+CAS Attack on the Minimum Kochen–Specker Problem (preprint) (Update June 23, 2023) [bib]
- November 14, 2022 Proceedings of SC-Square 2021: The 6th International Workshop on Satisfiability Checking and Symbolic Computation (Preface) [contents, bib] editor
- September 13, 2022 Success Guide for COMP-1410, Fall 2022 (Updated Fall 2023)
- May 28, 2022 Enumerating Projective Planes of Order Nine with Proof Verification (extended abstract preprint) workshop
- May 28, 2022 An SC-Square Approach to the Minimum Kochen–Specker Problem (extended abstract preprint) workshop
- March 25, 2022 Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation conference
- October 12, 2021 Hadamard 160 in Cool Tones conference invited judges' choice award
- October 6, 2021 Improving Integer and Constraint Programming for Graeco-Latin Squares [bib] conference
- September 17, 2021 Integer and Constraint Programming Revisited for Mutually Orthogonal Latin Squares (student abstract) [bib] conference
- March 19, 2021 Integer and Constraint Programming Revisited for Mutually Orthogonal Latin Squares (preprint) [errata]
- November 1, 2020 NSERC Discovery Grant Proposal
- September 16, 2020 When Satisfiability Solving Meets Symbolic Computation: The Science of Less-Than-Brute Force [bib] journal
- September 11, 2020 A SAT-based Resolution of Lam's Problem [bib] conference
- May 29, 2020 Knowledge Representation in the Search for Projective Geometries
- May 2, 2020 Lam's Problem Benchmarks for the SAT Competition 2020
- January 24, 2020 Nonexistence Certificates for Ovals in a Projective Plane of Order Ten [bib] conference
- January 22, 2020 Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem [bib] conference
- November 10, 2019 A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords [bib, errata] journal best paper award
- September 4, 2019 A SAT Certification for the Nonexistence of Weight 16 Codewords in a Projective Plane of Order Ten (preprint) [bib, errata]
- June 24, 2019 SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics [bib] conference
- June 13, 2019 Effective Problem Solving Using SAT Solvers [bib] conference
- May 10, 2019 Searching for Projective Planes with Computer Algebra and SAT Solvers (abstract)
- May 1, 2019 New Infinite Families of Perfect Quaternion Sequences and Williamson Sequences [bib] journal
- March 20, 2019 Research Statement of Curtis Bright [extended]
- March 11, 2019 The SAT+CAS Method for Combinatorial Search with Applications to Best Matrices [bib, errata] journal
- February 26, 2019 A Verifiable Search for Projective Planes of Order Ten [bib]
- February 13, 2019 The Best Matrix Conjecture
- November 24, 2018 Complex Golay Pairs up to Length 28: A Search via Computer Algebra and Programmatic SAT [bib] journal
- October 15, 2018 NSERC Postdoctoral Fellowships Program Application
- September 18, 2018 A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples [bib] conference
- June 15, 2018 The SAT+CAS Paradigm and the Williamson Conjecture (extended abstract) [bib] journal
- May 14, 2018 Enumeration of Complex Golay Pairs via Programmatic SAT [bib, errata] conference
- March 19, 2018 Applying Computer Algebra Systems with SAT Solvers to the Williamson Conjecture [bib] journal
- March 4, 2018 A Doubling Construction for Williamson Matrices [bib]
- November 20, 2017 A SAT+CAS Method for Enumerating Williamson Matrices of Even Order [bib] conference
- November 19, 2017 A New Form of Williamson's Product Theorem [bib]
- July 11, 2017 A SAT+CAS Method for Enumerating Williamson Matrices of Even Order (preprint) workshop
- April 27, 2017 Computational Methods for Combinatorial and Number Theoretic Problems [bib, webpage] thesis
- December 9, 2016 New Results on Complex Golay Pairs [bib]
- November 19, 2016 Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures [bib] journal invited
- September 20, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures [bib] conference invited
- August 14, 2016 Searching for Complex Golay Sequences Using a SAT Solver
- July 15, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures [bib] workshop
- February 29, 2016 PhD Research Proposal
- January 17, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (preprint)
- September 27, 2014 Minimal Elements for the Prime Numbers [bib] journal
- April 10, 2014 Exceptional Examples in the
`abc`Conjecture [bib] - April 15, 2013 Computing the Galois Group of a Polynomial [bib]
- April 21, 2012 The Quartic Formula Derivation [bib, webpage]
- April 2, 2012 8*13^(4*8005)+183 is a Probable Prime
- December 29, 2011 From the Shortest Vector Problem to the Dihedral Hidden Subgroup Problem [bib]
- April 20, 2011 Passing Arguments: A Comparison Among Programming Languages [bib]
- March 30, 2011 Vector Rational Number Reconstruction [bib, errata] conference
- December 20, 2010 Automated Construction of Phylogenetic Trees [bib]
- December 13, 2010 Ataxx with AI [webpage]
- August 31, 2009 Vector Rational Number Reconstruction
- April 29, 2009 Reduction of Lattice Bases [bib]
- April 16, 2009 Neural Networks for Insurance Fraud Detection [bib]
- December 15, 2008 Algorithms for Lattice Basis Reduction
- July 20, 2008 Notes on Chapter 2 of Ideals, Varieties and Algorithms
- April 24, 2008 Modular Periodicity of Linear Recurrence Sequences
- April 18, 2008 Insurance Fraud Statistics
- February 12, 2008 Solving Ramanujan's Square Equation Computationally [bib, webpage]
- September 12, 2007 Finding Generalized Near-Repdigit Squares

# Showcase

Apps, videos, and posters that I've composed to showcase my research and some of its applications. I enjoy bringing life to my research by using accessible visualizations and interactivity.

`n`-Queens Problem October 4, 2018

# Talks

An archive of my academic talks that have used slides.

- July 18, 2024 SAT and Lattice Reduction for Integer Factorization ISSAC, Raleigh, USA conference
- June 27, 2023 SAT and Computer Algebra Dagstuhl Seminar, Wadern, Germany invited
- June 6, 2023 A SAT and Orderly Generation Approach in the Quest for the Minimum Kochen–Specker System CanaDAM, University of Winnipeg, Winnipeg, Manitoba conference invited
- June 5, 2023 Solving
`n`-Queens using a SAT solver in SageMath [worksheet] Impromptu talk in the Computer-Assisted Mathematics Minisymposium CanaDAM, University of Winnipeg, Winnipeg, Manitoba conference - June 5, 2023 A New Lower Bound in the
`abc`Conjecture CanaDAM, University of Winnipeg, Winnipeg, Manitoba conference - May 14, 2023 SAT Solving + Isomorph-free Generation ...and the Quest for the Minimum Kochen–Specker System Quantum Computing Academic Assembly invited
- April 20, 2023 SAT + Isomorph-free Generation ...and the Quest for the Minimum Kochen–Specker System Dagstuhl Seminar, Wadern, Germany invited
- February 8, 2023 SAT Solvers, Isomorph-free Generation, and the Quest for the Minimum Kochen–Specker System [abstract] SFU, Vancouver, British Columbia invited
- February 7, 2023 SAT Solvers, Isomorph-free Generation, and the Quest for the Minimum Kochen–Specker System [abstract] UBC, Vancouver, British Columbia invited
- August 15, 2022 Searching for Kochen–Specker Systems With Orderly Generation and Satisfiability Solving ACA, Gebze Technical University, Istanbul, Turkey; Presented Online conference
- August 3, 2022 Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation [video] Israel Institute of Technology, Haifa, Israel; Presented Online conference
- June 16, 2022 Searching for Kochen–Specker Systems With Orderly Generation and Satisfiability Solving [abstract] Simons Institute, Berkeley, USA invited
- April 1, 2022 SAT Solving with Computer Algebra for Combinatorics [video, abstract] Tutte Colloquium, Waterloo, Ontario; Presented Online invited
- February 17, 2022 Isomorph-Free Exhaustive Generation in SAT Solving [video, abstract] Invited Tutorial at Dagstuhl Seminar, Wadern, Germany; Presented Online invited
- November 3, 2021 When Computer Algebra Meets Satisfiability: A New Approach to Combinatorial Mathematics [video, abstract] Harvard University, Cambridge, USA; Presented Online invited
- July 14, 2021 Satisfiability Checking + Symbolic Computation: A New Approach to Combinatorial Mathematics Rice University, Houston, USA; Presented Online invited
- May 25, 2021 SAT Solvers and Combinatorics Problems [script, video] CanaDAM; Presented Online conference invited
- May 6, 2021 Computational Algebra and Logic for Mathematical Search UWindsor, Windsor, Ontario; Presented Online invited
- April 21, 2021 Computer Algebra and SAT for Mathematical Search [video] Simons Institute, Berkeley, USA; Presented Online workshop invited
- February 3, 2021 A SAT-based Resolution of Lam's Problem [video] [extended, video] AAAI, Vancouver, British Columbia; Presented Online conference
- January 14, 2021 Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem (highlights) [video] IJCAI, Yokohama, Japan; Presented Online conference
- January 6, 2021 Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem [video] IJCAI, Yokohama, Japan; Presented Online conference
- December 4, 2020 A Resolution of Lam's Problem via Satisfiability Solvers [video] Canadian Mathematical Society Meeting, Montréal, Québec; Presented Online conference invited
- June 8, 2020 Nonexistence Certificates for Ovals in a Projective Plane of Order Ten [video] IWOCA, Bordeaux, France; Presented Online conference
- March 12, 2020 SAT Solving with Computer Algebra for Fast, Verified Mathematical Search UWindsor, Windsor, Ontario invited
- March 12, 2020 Introduction to Polymorphism in Object-Oriented Programming UWindsor, Windsor, Ontario
- February 28, 2020 SAT Solving with Computer Algebra and its Application to Graph Theory and Geometry CGLAB, Ottawa, Ontario invited
- November 4, 2019 SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics CASCON, Markham, Ontario conference
- October 17, 2019 Effective Problem Solving Using SAT Solvers [pdf, video] Maple Conference, Waterloo, Ontario conference
- September 10, 2019 SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method UBC, Vancouver, British Columbia invited
- September 6, 2019 SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method UVic, Victoria, British Columbia invited
- September 3, 2019 SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method SFU, Vancouver, British Columbia invited
- July 19, 2019 Searching for Projective Planes with Computer Algebra and SAT Solvers ACA, Montréal, Québec conference
- January 30, 2019 A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples [extended] AAAI, Honolulu, USA conference
- October 5, 2018 SAT+CAS: A Powerful New Combinatorial Search Method Carleton, Ottawa, Ontario invited
- August 31, 2018 Faster SAT Solving with Applications to Sudoku [pdf] Maplesoft, Waterloo, Ontario invited
- July 26, 2018 MathCheck: A SAT+CAS Mathematical Conjecture Verifier ICMS, Notre Dame, USA conference
- July 17, 2018 Enumeration of Complex Golay Pairs via Programmatic SAT ISSAC, New York, USA conference
- March 23, 2018 Improvements to Satisfy and ChromaticNumber [pdf] Maplesoft, Waterloo, Ontario invited
- February 4, 2018 A SAT+CAS Method for Enumerating Williamson Matrices of Even Order AAAI, New Orleans, USA conference
- July 29, 2017 A SAT+CAS Method for Enumerating Williamson Matrices of Even Order SC
^{2}Workshop, Kaiserslautern, Germany workshop - March 23, 2017 Computational Methods for Combinatorial and Number Theoretic Problems thesis
- December 7, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- December 7, 2016 Minimal Elements for the Prime Numbers
- November 18, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- September 24, 2016 MathCheck2: Combining Learning-based Search (SAT) with Symbolic Computation (CAS) SC
^{2}Workshop, Timișoara, Romania workshop - September 20, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures CASC, Bucharest, Romania conference
- July 12, 2016 MathCheck: A Math Assistant Combining SAT with Computer Algebra Systems IJCAI, New York, USA conference
- July 2, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures SMT Workshop, Coimbra, Portugal workshop
- May 13, 2016 MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures ACMES, London, Ontario workshop
- March 14, 2016 PhD Research Proposal: A SAT+CAS System for Checking Math Conjectures
- March 27, 2014 Extremal Examples in the
`abc`Conjecture - September 9, 2013 Proving the Prime Number Theorem in an Hour
- April 8, 2013 Computing the Galois Group of a Polynomial
- December 8, 2011 From the Shortest Vector Problem to the Dihedral Hidden Subgroup Problem
- June 9, 2011 Vector Rational Number Reconstruction ISSAC, San Jose, USA conference
- August 28, 2009 Vector Rational Number Reconstruction: Version 2
- August 20, 2009 Vector Rational Number Reconstruction
- May 21, 2009 Lattice Basis Reduction and the LLL Algorithm
- July 31, 2008 LLL overview: Lenstra-Lenstra-Lovász Lattice Basis Reduction
- July 3, 2008 Notes on Chapter 2 of Ideals, Varieties and Algorithms

# Bio

In August 2021, I co-chaired (with James Davenport) the 2021 SC-square workshop. In the fall of 2021, I taught a graduate course on computational discrete mathematics. In the winter of 2022, and again in the summer of 2022, I taught *Key Concepts in Computer Science* and *Introduction to Algorithms and Programming II*. I taught *Prog II* again in fall 2022, along with a graduate course in computer algebra and computational mathematics.

In July 2021, I became an adjunct research professor in the School of Mathematics and Statistics at Carleton University. In Winter 2022, an undergraduate student I supervised, Noah Rubin, defended his Bachelor's thesis; he is now a full time software developer for Canada's cryptologic agency.

I joined the faculty of the School of Computer Science at the University of Windsor in 2020 and taught *Introduction to Algorithms and Programming II* in the winter of 2021.

I am currently the lead developer of the MathCheck project run by professor Vijay Ganesh at the University of Waterloo. In 2020, I held an NSERC postdoctoral fellowship at Carleton University working with professors Kevin Cheung and Brett Stevens. Our major result was generating and verifying the first set of nonexistence certificates for solving Lam's problem.

Between 2017 and 2019, I was a postdoctoral fellow of the Computer Aided Research Group at the University of Waterloo. I was also affiliated with the CARGO Lab at Wilfrid Laurier University and worked with professor Ilias Kotsireas on combinatorial matrix theory. During this time, I devised the first proof that Williamson matrices exist in all orders that are powers of two.

I interned at Maplesoft in 2017 and again in 2018. While at Maplesoft I applied my research to dramatically improve some discrete optimization routines of Maple—for example, in the latest version of Maple the chromatic number of the Queen Graph of the chessboard can be computed in a few seconds instead of a few hours. I have written a number of Maple applications demonstrating how to effectively use Maple's SAT solver in a variety of problems and presented many of these applications at the 2019 Maple conference.

In March 2017, I defended my PhD thesis, supervised by Vijay Ganesh and Krzysztof Czarnecki. My thesis demonstrated the effectiveness of combining satisfiability checking and symbolic computation for solving mathematical problems.

In Fall 2015, I taught Elementary Algorithm Design and Data Abstraction alongside Gordon Cormack to 258 students. This course is the follow-up to Designing Functional Programs intended for CS and math majors and uses the programming language C.

In Summer 2015, I was the sole instructor of 145 students in Introduction to Computer Science 1, an introduction to computer science intended for non-CS majors. As the instructor I was responsible for compiling 9 assignments throughout the term and each one consisted of questions newly developed by myself.

In Fall 2014, I taught Designing Functional Programs, an introduction to computer science for CS and math majors based around the programming language Racket. I coordinated with 5 other instructors to teach 876 students.

In Summer 2014, as a part of Google's summer of code I supervised (along with William Hart) the undergraduate student Abhinav Baid and oversaw the implementation of a fast variant of the LLL algorithm for lattice basis reduction in the open source number theory library FLINT. This code is available in the latest version of FLINT in the `fmpz_lll` module.

In Spring 2013, I received an award for exceptional performance as an instructional assistant in the course Logic and Computation. During this term I wrote an online truth table generator for easily generating truth tables to include in assignment solutions and course notes.

In Winter 2013, I designed the SCG logo (a spoof on a proposed UW logo). At the time I was a graduate student and I've made publicly available a collection of the lecture notes that I took as a student.

In 2007, I started a personal website for nonacademic projects, though most of my effort these days goes into advancing my research program.

# Awards

I won the Application of Computer Algebra Early Researcher Award at ACA 2022.

At the Maple Conference 2021 Mathematical Art and Creative Works Exhibit my submission with Bridjet Lee won the judges' choice award.

My 2020 paper A nonexistence certificate for projective planes of order ten with weight 15 codewords won the Jacques Calmet best paper award.

**Bragging rights:** My Erdős number is 2, through the papers Minimal elements for the prime numbers (Bright, Devillers, Shallit) and New bounds on the length of finite Pierce and Engel series (Erdős, Shallit). I have been awarded 0x$1.20 at Knuth's Bank of San Serriffe for finding a typo in The Art of Computer Programming present since the first edition (!) of volume 2 in 1969. In the 2015 version of his classic text Galois Theory, Ian Stewart cited a report of mine. Additionally, Noam Elkies once gave a talk referencing a result that I showed as an undergraduate student—the technical report is dear to my heart as one of the first papers I ever wrote.