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
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.
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.
Interactive Molecular Dynamics
physics.weber.edu
November 10, 2025 at 5:16 PM
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.
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.
3 Philosophers is my all time favorite! We keep a few in the house to celebrate new grants / papers.
August 8, 2025 at 10:41 AM
3 Philosophers is my all time favorite! We keep a few in the house to celebrate new grants / papers.
Haha, me too!
August 2, 2025 at 2:53 PM
Haha, me too!
I guess it’s not “Google-proof” after all
April 3, 2025 at 11:15 AM
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.
March 14, 2025 at 10:16 AM
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.
@blaneylab.bsky.social and Upal Ghosh - I think this is the paper I had in mind: www.sciencedirect.com/science/arti...
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…
www.sciencedirect.com
March 14, 2025 at 10:11 AM
@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.
March 14, 2025 at 1:23 AM
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?”
March 13, 2025 at 1:57 AM
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?”
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...)
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
February 25, 2025 at 4:17 PM
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...)
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...)
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
February 25, 2025 at 4:09 PM
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...)
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...
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...
www.youtube.com
February 13, 2025 at 2:54 AM
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...