Tyler R. Josephson 藍泰來 (he/him)
@atomslab.bsky.social
AI & Theory-Oriented Molecular Science. Asst Prof at UMBC, molecular simulations for the environment + automated reasoning for chemical science and engineering. RT≠PV/n
https://atomslab.github.io
https://atomslab.github.io
I'm honored to be a @simonsfoundation.org Pivot Fellow! With this award, I'll be mentored by Jeremy Avigad at @cmu.edu. I’ll study formal methods and mathematics, to deepen my understanding of proofs and the Lean programming language, and apply this to formalizing scientific computing in Lean.
November 15, 2025 at 5:35 AM
I'm honored to be a @simonsfoundation.org Pivot Fellow! With this award, I'll be mentored by Jeremy Avigad at @cmu.edu. I’ll study formal methods and mathematics, to deepen my understanding of proofs and the Lean programming language, and apply this to formalizing scientific computing in Lean.
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Over 1100 people around the world, virtual and in-person, decided to take a chance together, to imagine, and build - seeking ways to speed discovery and understanding in materials and chemistry with AI.
We'll share our findings soon, but from what I've heard already prepare to be amazed.
We'll share our findings soon, but from what I've heard already prepare to be amazed.
September 10, 2025 at 3:43 PM
Over 1100 people around the world, virtual and in-person, decided to take a chance together, to imagine, and build - seeking ways to speed discovery and understanding in materials and chemistry with AI.
We'll share our findings soon, but from what I've heard already prepare to be amazed.
We'll share our findings soon, but from what I've heard already prepare to be amazed.
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Our latest Best Practices article "Developing Monte Carlo Methodologies in Molecular Simulations" is out now and describes how to derive acceptance probabilities for a variety of Monte Carlo moves:
doi.org/10.33011/liv...
#compchem
doi.org/10.33011/liv...
#compchem
August 11, 2025 at 6:32 PM
Our latest Best Practices article "Developing Monte Carlo Methodologies in Molecular Simulations" is out now and describes how to derive acceptance probabilities for a variety of Monte Carlo moves:
doi.org/10.33011/liv...
#compchem
doi.org/10.33011/liv...
#compchem
Reposted by Tyler R. Josephson 藍泰來 (he/him)
New paper: "Large Language Models and Emergence: A Complex Systems Perspective" (D. Krakauer, J. Krakauer, M. Mitchell).
We look at claims of "emergent capabilities" & "emergent intelligence" in LLMs from the perspective of what emergence means in complexity science.
arxiv.org/pdf/2506.11135
We look at claims of "emergent capabilities" & "emergent intelligence" in LLMs from the perspective of what emergence means in complexity science.
arxiv.org/pdf/2506.11135
arxiv.org
June 16, 2025 at 1:15 PM
New paper: "Large Language Models and Emergence: A Complex Systems Perspective" (D. Krakauer, J. Krakauer, M. Mitchell).
We look at claims of "emergent capabilities" & "emergent intelligence" in LLMs from the perspective of what emergence means in complexity science.
arxiv.org/pdf/2506.11135
We look at claims of "emergent capabilities" & "emergent intelligence" in LLMs from the perspective of what emergence means in complexity science.
arxiv.org/pdf/2506.11135
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. arxiv.org/abs/2504.06239 #ITP #LeanProver #Math
Canonical for Automated Theorem Proving in Lean
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to generate proof terms...
arxiv.org
April 10, 2025 at 3:07 PM
Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. arxiv.org/abs/2504.06239 #ITP #LeanProver #Math
This has been a really fun project to work on! Having a great time building with an effective team!
A multidisciplinary team led by UMBC researchers was awarded $3.8M from DARPA's SciFy: Scientific Feasibility program to explore new computational methods for assessing the feasibility of scientific claims. umbc.edu/quick-posts/...
UMBC team leads research into AI tools that can assess the feasibility of scientific claims
A multidisciplinary team of UMBC researchers was recently awarded $3.8 million from the Defense Advanced Research Projects Agency (DARPA) to develop new computational methods for assessing the feasibi...
umbc.edu
April 4, 2025 at 7:45 PM
This has been a really fun project to work on! Having a great time building with an effective team!
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Quantum harmonic oscillator in Lean: heplean.com/CuratedNotes...
PhysLean: Digitalizing Physics in Lean 4
A project to digitalize results from physics into Lean 4.
heplean.com
March 5, 2025 at 9:32 AM
Quantum harmonic oscillator in Lean: heplean.com/CuratedNotes...
Reposted by Tyler R. Josephson 藍泰來 (he/him)
February 27, 2025 at 5:26 PM
This is one of my favorite slides from Lean for Scientists and Engineers. Traditionally, people imagine new scientific theories, derive them by hand, and implement them in software as best as they can, then compare to experiment. But this is hard, and people can make mistakes along the way!
February 25, 2025 at 4:17 PM
This is one of my favorite slides from Lean for Scientists and Engineers. Traditionally, people imagine new scientific theories, derive them by hand, and implement them in software as best as they can, then compare to experiment. But this is hard, and people can make mistakes along the way!
Very accessible! Definitely sharing this with my students.
Modern-Day Oracles or Bullshit Machines?
Jevin West (@jevinwest.bsky.social) and I have spent the last eight months developing the course on large language models (LLMs) that we think every college freshman needs to take.
thebullshitmachines.com
Jevin West (@jevinwest.bsky.social) and I have spent the last eight months developing the course on large language models (LLMs) that we think every college freshman needs to take.
thebullshitmachines.com
INTRODUCTION
thebullshitmachines.com
February 4, 2025 at 7:20 PM
Very accessible! Definitely sharing this with my students.
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Modern-Day Oracles or Bullshit Machines?
Jevin West (@jevinwest.bsky.social) and I have spent the last eight months developing the course on large language models (LLMs) that we think every college freshman needs to take.
thebullshitmachines.com
Jevin West (@jevinwest.bsky.social) and I have spent the last eight months developing the course on large language models (LLMs) that we think every college freshman needs to take.
thebullshitmachines.com
INTRODUCTION
thebullshitmachines.com
February 4, 2025 at 4:12 PM
Modern-Day Oracles or Bullshit Machines?
Jevin West (@jevinwest.bsky.social) and I have spent the last eight months developing the course on large language models (LLMs) that we think every college freshman needs to take.
thebullshitmachines.com
Jevin West (@jevinwest.bsky.social) and I have spent the last eight months developing the course on large language models (LLMs) that we think every college freshman needs to take.
thebullshitmachines.com
Reposted by Tyler R. Josephson 藍泰來 (he/him)
New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili. adam.math.hhu.de#/g/jadabouha... #ITP #LeanProver
January 28, 2025 at 11:47 AM
New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili. adam.math.hhu.de#/g/jadabouha... #ITP #LeanProver
I've uploaded a few more lectures on Lean for Scientists and Engineers: youtube.com/playlist?lis...
Lectures 2-4 cover how to write proofs in Lean to reason about equalities, inequalities, and basic logic (and, or, implies, exists, etc.), and illustrate with examples in science and engineering.
Lectures 2-4 cover how to write proofs in Lean to reason about equalities, inequalities, and basic logic (and, or, implies, exists, etc.), and illustrate with examples in science and engineering.
Lean for Scientists and Engineers 2024 - YouTube
Lean 4 is a programming language whose type system enables it to check complicated math proofs. This ~22-hour lecture series is an introduction to Lean for n...
youtube.com
January 23, 2025 at 6:10 PM
I've uploaded a few more lectures on Lean for Scientists and Engineers: youtube.com/playlist?lis...
Lectures 2-4 cover how to write proofs in Lean to reason about equalities, inequalities, and basic logic (and, or, implies, exists, etc.), and illustrate with examples in science and engineering.
Lectures 2-4 cover how to write proofs in Lean to reason about equalities, inequalities, and basic logic (and, or, implies, exists, etc.), and illustrate with examples in science and engineering.
Reposted by Tyler R. Josephson 藍泰來 (he/him)
I've been thinking about how reasoning models will change AI applied to science. The recent papers from Deepseek/AI2/MoonShotAI are showing that we can exceed humans on reasoning tasks and I've written up some reflections on the consequences
diffuse.one/p/d1-007
diffuse.one/p/d1-007
diffuse.one
andrew white's blog.
diffuse.one
January 21, 2025 at 5:32 PM
I've been thinking about how reasoning models will change AI applied to science. The recent papers from Deepseek/AI2/MoonShotAI are showing that we can exceed humans on reasoning tasks and I've written up some reflections on the consequences
diffuse.one/p/d1-007
diffuse.one/p/d1-007
Interested in learning a new programming language that enables you to prove the code you've written is correct?
I taught "Lean for Scientists and Engineers" in Summer 2024. Soon, we'll have all the lectures on YouTube! Here's the first one: www.youtube.com/watch?v=s9Dy...
I taught "Lean for Scientists and Engineers" in Summer 2024. Soon, we'll have all the lectures on YouTube! Here's the first one: www.youtube.com/watch?v=s9Dy...
Lean for Scientists and Engineers, Summer 2024 - Lecture 1
YouTube video by Tyler Josephson
www.youtube.com
January 6, 2025 at 5:49 AM
Interested in learning a new programming language that enables you to prove the code you've written is correct?
I taught "Lean for Scientists and Engineers" in Summer 2024. Soon, we'll have all the lectures on YouTube! Here's the first one: www.youtube.com/watch?v=s9Dy...
I taught "Lean for Scientists and Engineers" in Summer 2024. Soon, we'll have all the lectures on YouTube! Here's the first one: www.youtube.com/watch?v=s9Dy...
We’re working on this! Just kicked off the DARPA SciFy project last week: 5 teams building AIs and 1 team making novel, challenging benchmarks. Expect major progress in the next year. www.darpa.mil/research/pro...
December 17, 2024 at 3:30 AM
We’re working on this! Just kicked off the DARPA SciFy project last week: 5 teams building AIs and 1 team making novel, challenging benchmarks. Expect major progress in the next year. www.darpa.mil/research/pro...
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Poem by Joseph Fasano
November 29, 2024 at 8:57 PM
Poem by Joseph Fasano
Reposted by Tyler R. Josephson 藍泰來 (he/him)
Reflections from the 2024 Large Language Model (LLM) Hackathon for Applications in Materials Science and Chemistry
arxiv.org/abs/2411.15221 #compchem
arxiv.org/abs/2411.15221 #compchem
Reflections from the 2024 Large Language Model (LLM) Hackathon for Applications in Materials Science and Chemistry
Here, we present the outcomes from the second Large Language Model (LLM) Hackathon for Applications in Materials Science and Chemistry, which engaged participants across global hybrid locations, resul...
arxiv.org
November 26, 2024 at 7:32 AM
Reflections from the 2024 Large Language Model (LLM) Hackathon for Applications in Materials Science and Chemistry
arxiv.org/abs/2411.15221 #compchem
arxiv.org/abs/2411.15221 #compchem
Hi! I lead the AI & Theory-Oriented Molecular Science (ATOMS) Lab at UMBC! We develop methods for simulating adsorption of water pollutants, and we're bringing automated reasoning into chemical sciences and engineering. Check out our group at atomslab.github.io
ATOMS Lab @ UMBC
This is the official web page for the ATOMS Lab at UMBC.
atomslab.github.io
November 24, 2024 at 2:10 AM
Hi! I lead the AI & Theory-Oriented Molecular Science (ATOMS) Lab at UMBC! We develop methods for simulating adsorption of water pollutants, and we're bringing automated reasoning into chemical sciences and engineering. Check out our group at atomslab.github.io