Tyler R. Josephson 藍泰來 (he/him)

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.

It sounds like you’re already having them use more advanced simulation tools, but I use this browser-based one in my class:

physics.weber.edu/schroeder/md...

Supports ensemble average properties of 2D LJ fluid, liquid droplet in vapor, phase changes with T, finite size effects, etc.

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.

Table of contents figure

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

3 Philosophers is my all time favorite! We keep a few in the house to celebrate new grants / papers.

Haha, me too!

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

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

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!

I guess it’s not “Google-proof” after all

The multicomponent aspect is really interesting, I think. Sucralose is a strong signal for “came from cities/toilets” while other molecules may come from industrial, municipal, and/or agricultural sources.

Geospatial and co-occurrence analysis of antibiotics, hormones, and UV filters in the Chesapeake Bay (USA) to confirm inputs from wastewater treatment plants, septic systems, and animal feeding operat... Previous studies have reported select contaminants of emerging concern (CECs) in limited areas of the Chesapeake Bay (USA), but no comprehensive effor…

@blaneylab.bsky.social and Upal Ghosh - I think this is the paper I had in mind: www.sciencedirect.com/science/arti...

That’s a decent description of Lean 3, but Lean 4 is a full-fledged functional programming language. It has lists, strings, I/O, floats, etc. - all useful for writing programs.

Ooh! My colleagues work on similar problems on the rivers flowing into the Chesapeake Bay. They also have the added questions of “which pollutants are coming from where?” and “where would be the best places to put multiple detectors?”

Quantum harmonic oscillator in Lean: heplean.com/CuratedNotes...

This is a cartogram map of the United States depicting land use by different categories. The map distorts state shapes to represent proportional land usage. Key land use types include cow pasture/range (covering much of the central U.S.), private and federal timberland in the Pacific Northwest, corporate timberland in the Southeast, and urban housing/commercial areas in the Northeast. Other categories include agriculture (livestock feed, wheat exports, ethanol/biodiesel, cotton), protected lands (national parks, federal wilderness, state parks), and infrastructure (railroads, airports, highways). Additional specialized land uses include wildfires, golf courses, Christmas tree farms, and maple syrup production.

I think about this map a lot.

www.bloomberg.com/graphics/201...

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

Instead, could we validate the construction of math, scientific models, and software in one system? With Lean 4's ability to unify proofs and programs, we can! (This is from Lecture 3: check out the whole course here! youtube.com/playlist?lis...)

Flowchart illustrating relationship among pure math, scientific models, scientific software, and reality. In the realm of pure math, syntax separates logically valid statements from all possible combinations of symbolic. Logically valid statements bridge into symbolic scientific models, which also need to bridge to computable models. Computable models are implemented as code in scientific software, which finally bridges to reality. A final bridge does connect symbolic models directly to reality, but the main path is via computable models and code.

The previous chart, with three boxes overlaid. Traditionally, the validity of the mathematics and the scientific theory are established by hand. Humans read the theory and write the code as best as they can. Then use various automated and manual means to compare to experiment.

The three overlaid boxes have been replaced with just two: Can we represent all of this in Lean, and validate the construction of the math, scientific models, and software, in one system? Then use various automated and manual means to compare to experiment.

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!

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

Instead, could we validate the construction of math, scientific models, and software in one system? With Lean 4's ability to unify proofs and programs, we can! (This is from Lecture 3: check out the course here! youtube.com/playlist?lis...)

Principles of Dynamic Heterogeneous Catalysis: Surface Resonance and Turnover Frequency Response Acceleration of the catalytic transformation of molecules via heterogeneous materials occurs through design of active binding sites to optimally balance the requirements of all steps in a catalytic cy...

pubs.acs.org/doi/10.1021/...

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

If you want to check out another resource for learning Lean, check out the course I taught last summer, Lean for Scientists and Engineers: www.youtube.com/playlist?lis...

Very accessible! Definitely sharing this with my students.

INTRODUCTION

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

New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili. adam.math.hhu.de#/g/jadabouha... #ITP #LeanProver

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

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.

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

GitHub - ATOMSLab/LFSE2024: Lean for Scientists and Engineers, course taught in Summer 2024 Lean for Scientists and Engineers, course taught in Summer 2024 - ATOMSLab/LFSE2024

I'll be getting more videos up over the coming weeks. In the meantime, the code and slides from the whole course are here:

github.com/ATOMSLab/LFS...

YouTube video by Tyler Josephson Lean for Scientists and Engineers, Summer 2024 - Lecture 1

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

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