Tanbir Ahmed, Ph. D.

About

Greetings and welcome to my research homepage! Delighted to have you here.

Currently: Generative AI Expert at Morgan Stanley

I am a Generative AI expert, an experimental mathematician, and a computer scientist specializing in Extremal Combinatorics, Combinatorial Optimization, Automated Reasoning, and High Performance Computing.

At Morgan Stanley, I apply advanced generative AI techniques to solve complex financial and computational challenges. My background combines deep expertise in experimental mathematics, computer science, and automated reasoning with practical experience in enterprise AI systems.

My research applies computational and symbolic methods to solve deep mathematical problems that have resisted traditional proof techniques. Many of my results are computer-generated or computer-assisted—demonstrating that rigorous mathematics and automated reasoning are complementary forces. This foundation now informs my work in developing scalable, interpretable AI solutions for real-world applications.

My journey into research began during my undergraduate days at BUET, Bangladesh, under the guidance of Prof. M. Kaykobad. In Canada, I pursued my M.Sc. in Computer Science (2007-2009) at Concordia University, where I had the privilege of conducting research in Combinatorial Optimization under the supervision of Prof. Vašek Chvátal. Continuing my academic journey, I earned my Ph.D. in Computer Science (2010-2013) at Concordia University, focusing on extremal combinatorics under the mentorship of Prof. Clement Lam. During the years 2011 to 2013, I engaged in intensive online collaboration in Combinatorics with Prof. Hunter Snevily.

From 2013 to 2015, I continued my research journey as a research associate at Concordia. Subsequently, I served as a post-doctoral researcher at Le Laboratoire d'Algèbre, de Combinatoire et d'Informatique Mathématique (LACIM) from 2015 to 2018.

Recently, I have worked as a Research Associate in the School of Computer Science at the University of Windsor hosted by Prof. Curtis Bright

I am passionate about collaborating online with fellow mathematicians and computer scientists, tackling various intriguing problems. Many of these problems involve extensive coding for data generation and analysis. In fact, most of my mathematical results are either wholly generated by computers or at least greatly assisted by them.

Scientific Contributions:

🧊Foundations of the Cube-and-Conquer SAT Solving Paradigm
Originally, I applied divide-and-conquer technique for large-scale distributed SAT-solving for computation of van der Waerden numbers (2010). A generalization of this method (known as the Cube-and-Conquer method) partitioning hard SAT instances into thousands of subproblems for parallel solving has become the standard approach for intractable combinatorial problems including the Boolean Pythagorean Triples problem and modern Ramsey theory computations.
📊Computational Ramsey Theory
Established previously unknown van der Waerden numbers, including w(2;3,17), w(2;3,18), w(2;3,19)=349, and 60+ others. My work is cited in Donald Knuth's The Art of Computer Programming at Volume 4, Fascicle 6: Chapter on Satisfiability and the accumulated exact values and lower bounds of w(2;3,k) worked as a catalyst to disprove the long-standing O(k²) conjecture via Ben Green's breakthrough lower-bound proof of w(2;3,k).
⚙️Automated Case-Based Proofs via Symbolic Sets
Developed AutoCase, a novel tool combining SymPy symbolic computation with Z3 SMT solving to automate extensive case-based proofs in Ramsey theory. Used to compute Rado numbers and prove lower bounds on 3-color Rado numbers for linear equations by constructing symbolic colorings that avoid monochromatic solutions. See Symbolic Sets and Rado's Theory for methodology and applications of automated case verification.
〰️Roller Coaster Permutations
Introduced roller coaster permutations with Hunter Snevily (2013), a novel combinatorial structure maximizing alternations. This sparked subsequent research including structural proofs and partition-theoretic applications, now cited in major journals.
🔒Solving Long-Standing Conjectures
Determined exact values and general properties for weak Schur numbers, and generalized Schur numbers.
💾Research Infrastructure & Open Science
Established 19+ sequences in the Online Encyclopedia of Integer Sequences (OEIS), developed tawSolver and other open-source tools, and curated extensive computational databases enabling researchers worldwide to tackle unsolved problems in extremal combinatorics and Ramsey theory.
🧠AI Explainability & Automated Reasoning
Bridges computer science and AI through work on explainable AI systems and the application of automated reasoning to real-world problems. Leverages expertise in symbolic computation and formal methods to build interpretable, trustworthy AI solutions for complex decision-making in finance and beyond.
My research interests are:

Generative AI • AI Explainability • Automated Reasoning • Symbolic Computation • Computer assisted proofs • Cryptographic Foundations • SAT and SMT Solving • Experimental Mathematics • Mathematical Programming • Integer & Zero-Sum Ramsey Theory • Discrete Mathematics
Contact:

Email: tanbir AT gmail DOT com