I solve mathematical problems and generate computer-assisted proofs using satisfiability solving and computer algebra. Currently, I am an assistant professor in the School of Computer Science at the University of Windsor and an adjunct research professor in the School of Mathematics and Statistics at Carleton University. I completed my PhD in the Cheriton School of Computer Science at the University of Waterloo and I remain the lead developer of 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.

**News:** The Algorithms & Mathematics group at Windsor is accepting applications for open research positions.

I co-chaired (with James Davenport) the 2021 SC-square workshop held on August 19–20, 2021.

# Published Works

My work has been published in a number of notable venues including in the Journal of Automated Reasoning, at the AAAI Conference on Artificial Intelligence 2018 (and 2019, 2021), at ISSAC 2018 (and 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.

**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.

# 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.

- January 26, 2023 A New Lower Bound in the
`abc`Conjecture submitted - November 16, 2022 A SAT+CAS Attack on the Minimum Kochenâ€“Specker Problem (preprint) submitted
- November 14, 2022 Proceedings of SC-Square 2021: The 6th International Workshop on Satisfiability Checking and Symbolic Computation (Preface) [contents, bib] editor
- 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 conference
- September 17, 2021 Integer and Constraint Programming Revisited for Mutually Orthogonal Latin Squares (student abstract) 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 The Science of Less-Than-Brute Force: When Satisfiability Solving Meets Symbolic Computation [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] 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 and posters that I've written 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.

- August 15, 2022 Searching for Kochen–Specker Systems With Orderly Generation and Satisfiability Solving 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

# Group

The following students are working or have worked in my group:

- Amadou Keita (PhD, current)
- Yameen Ajani (MSc, current)
- Nahiyan Alamgir (MSc, current)
- Usaid Rehman (MSc, current)
- Zhengyu Li (Waterloo MMath, current)
- Conor Duggan (Waterloo MMath, current)
- Vidyanshu Mishra (undergrad, summer intern)
- Shreyash Mutyalwar (undergrad, summer intern)
- Zhengyu Li (Toronto undergrad, graduated 2022, Project Report, presently a graduate student at Waterloo)
- Daniel Dallaire (Windsor undergrad, graduated 2022, Project Report, presently a graduate student at Ottawa)
- Noah Rubin (Carleton undergrad, graduated 2022, Honours Project, presently at Canada's national cryptologic agency CSC)

# Bio

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. 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.

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.