January Speaker

Integrated Systems for Computational Scientific Discovery: Progress, Challenges, and Implications

 Dr. Pat Langley, Georgia Tech Research Institute (GTRI)
January 30, 2026 | 4pm - 5pm  |Classroom 380, Bunger-Henry Building & online via Zoom

Abstract: There has been a steady stream of AI work on scientific discovery since the 1970s, much of it leading to published results in fields like astronomy, biology, chemistry, and physics. However, most efforts have focused on isolated tasks rather than addressing their interaction. In this talk, I challenge the research community to develop and adopt integrated discovery systems. I note distinguishing features of scientific discovery and examine five component abilities, in each case specifying the problem and reviewing results in the area. After this, I note some successes at partial integration and consider some remaining hurdles that we must leap to transform the vision for integrated discovery into reality. I also discuss promising domains, natural and synthetic, in which to test such computational artifacts. In closing, I consider ways that integrated discovery can aid the scientific enterprise and factors that influence whether results are trustworthy.

Bio: Dr. Pat Langley is a Principal Research Scientist at Georgia Tech Research Institute and Director of the Institute for the Study of Learning and Expertise. He has contributed to AI and cognitive science for more than 40 years, publishing over 300 papers and five books on these topics. Dr. Langley developed some of the first computational approaches to scientific knowledge discovery, and he was an early champion of experimental studies of machine learning and its application to real-world problems. He is the founding editor of two journals, Machine Learning in 1986 and Advances in Cognitive Systems in 2012, and he is a Fellow of both AAAI and the Cognitive Science Society. Dr. Langley's current research focuses on architectures for embodied agents, explainable, normative, and justified agency, and induction of dynamic process models from time series and background knowledge. 

Learn More and Access Zoom Link Here

February Speakers

Sequencelib: A Platform for Formalizing the OEIS

 Joe Stubbs, University of Texas at Austin

February 3, 2026 | 4pm - 5pm  |Classroom 380, Bunger-Henry Building & online via Zoom

Abstract: The On-Line Encyclopedia of Integer Sequences (OEIS) is a web-accessible database cataloging interesting integer sequences and associated theorems. With more than 390,000 sequences and 12,000 citations, the OEIS is one of the most robust and highly cited resources in all of theoretical mathematics. The Sequencelib project provides an open-source computational platform to formalize the mathematics contained within the OEIS using the Lean programming language. With contributions made through a combination of hand-written formalizations, metaprogramming, and AI, Sequencelib currently contains formalizations for more than 25,000 sequences and over 1.6 million theorems about their values. In this first of two talks, we will provide an introduction to the Sequencelib platform and describe its position within the Lean ecosystem, including its relationship to Mathlib, Lean's massive open-source library of formalized Mathematics. We will define precisely what is meant by "formalizing an OEIS sequence", and we will walk through the steps involved in a typical sequence formalization, showing how to use the primary Sequencelib facilities that support metadata collection and proof synthesis within the Lean interactive theorem prover. We will also discuss some of the interesting sequences that have been formalized in Sequencelib and survey some areas for future work and contributions.

Bio: Dr. Joe Stubbs is a Research Scientist at the University of Texas at Austin and leads the Cloud and Interactive Computing (CIC) group at the Texas Advanced Computing Center (TACC). CIC researches, builds and maintains national-scale cloud computing platforms and distributed systems for advanced research computing. He is the PI of multiple NSF-funded projects, and he leads TACC’s involvement in the NSF-funded ICICLE AI Institute. He also teaches courses and mentors students in the Computational Engineering program within the Cockrell School of Engineering at the University of Texas at Austin. His research and teaching focus on software engineering, scalable distributed systems design, formal methods and AI, and with Walter Moreira, he leads the Sequencelib project, a platform for formalizing the mathematics contained within the On-line Encyclopedia of Integer Sequences (OEIS) in the Lean 4 theorem prover.

Learn More and Access Zoom Link Here

Automated Formalization of OEIS using the Sequencelib Platform

 Walter Moreira, University of Texas at Austin

February 6, 2026 | 4pm - 5pm  | Classroom 183, J. Erskine Love Building & online via Zoom

Abstract: The On-Line Encyclopedia of Integer Sequences (OEIS) is a web-accessible database cataloging interesting integer sequences and associated theorems. With more than 390,000 sequences and 12,000 citations, the OEIS is one of the most robust and highly cited resources in all of theoretical mathematics. The Sequencelib project provides an open-source computational platform to formalize the mathematics contained within the OEIS using the Lean programming language. With contributions made through a combination of hand-written formalizations, AI and metaprogramming, Sequencelib currently contains formalizations for more than 25,000 sequences and over 1.6 million theorems about their values. In this second talk, we will provide an overview of the design and implementation of the metaprogramming capabilities in Sequencelib, including the OEIS attribute, which can be used to automatically attach OEIS sequence metadata to a Lean definition, and the oeis-tactic, which can be used to automatically prove theorems about the values of sequences. We also detail OEIS-LT, a lightweight, multi-threaded Lean tool server that bundles these capabilities into a scalable, machine-friendly API. Together, these tools support automated formalization workflows, and as an example, we describe the design and implementation of a computational pipeline that built on the work of Gauthier, et al. and leveraged OEIS-LT to formalize more than 25,000 sequences from the OEIS. .

Bio: Dr. Walter Moreira is a mathematician and software engineer that has experience across a wide spectrum of disciplines. With a background in pure mathematics, he has worked at the Astronomy Department at the University of Texas at Austin, the Texas Advanced Computing Center, and Canon Nanotechnologies, among other places. He specializes in developing software containing strong theoretical foundations and using formal methods. He is currently working on the formalization of the On-Line Encyclopedia of Integer Sequences. 

Learn More and Access Zoom Link Here