Stream: Geographic locality
Topic: Newark, DE, USA
Alena Gusakov (Sep 05 2020 at 22:49):
University of Delaware graduate in math and computer science here! Just realized this stream existed lol
Miles (Jan 18 2021 at 01:44):
Not too far away in Baltimore, MD
Tyler Josephson (Nov 16 2021 at 19:03):
Hey! I'm in Baltimore, too. Assistant prof in Chemical Engineering. https://cbee.umbc.edu/josephson/
Patrick Massot (Nov 16 2021 at 19:56):
Do you hope to explain chemistry to Lean?
Tyler Josephson (Nov 17 2021 at 16:07):
Yep! I just started training an undergrad Chemical Engineering student, who has been enjoying the Natural Number Game.
Arthur Paulino (Nov 17 2021 at 16:51):
Interesting! I'm curious to see what/how branches of chemistry can be formalized!
Julian Berman (Nov 17 2021 at 17:05):
What does doing so constitute, for someone who knows little about chemistry? Is the point to model formally some expected properties of combinations of elements and things, or yeah could someone perhaps educate what this means even!?
Yakov Pechersky (Nov 17 2021 at 17:15):
One thing could be to use formalized graph theory and group theory libraries to better describe chemical structure. What does a formal definition of "chirality" look like? Can one describe "atropisomerism" in a formal way? How consistent can one be wrt chemical structure without having to refer to quantum mechanics?
Yakov Pechersky (Nov 17 2021 at 17:16):
Another direction could be to formalize reactions and reaction schemes, having proofs that no atoms are made or lost in a reaction.
Yaël Dillies (Nov 17 2021 at 17:21):
Kekule structures as well are out there.
Yakov Pechersky (Nov 17 2021 at 17:34):
Those interested in applied computational chemistry and cheminformatics can check out GDB-13 and GDB-17, which seek to enumerate all molecules up to 13 or 17 atoms (given some constraints)
Tyler Josephson (Nov 17 2021 at 19:08):
My goal is to formalize various proofs and derivations in the chemical theory literature. Not so much "what are the fundamental axioms of chemistry on which everything else is built?" but instead "if I propose a model with assumptions X, can I prove Y?" A challenge will be to formalize our various assumptions (Lean should help with this), but do so while highlighting how these assumptions can have meaning in chemical contexts.
Tyler Josephson (Nov 17 2021 at 19:09):
For example, the first task I have given my student (no spoilers, here, please!) is to formalize the following derivation of the Langmuir adsorption isotherm:
1. S0 = S + SA # site balance
2. r_ads = k_ads * p * S # adsorption rate model
3. r_des = k_des * SA # desorption rate model
4. r_ads = r_des # equilibrium or steady-state assumption
5. p, k_ads, k_des, S0, S, SA > 0 (we know a priori that various terms are positive)
SA = S0 * (k_ads / k_des) * p / (1 + (k_ads / k_des) * p)
Substitute 2 and 3 into 4:
6. k_ads * p * S = k_des * SA
Solve for S
7. S = k_des * SA / k_ads / p
Substitute 7 into 1
8. S0 = k_des * SA / k_ads / p + SA
Solve for SA:
9. SA = S0 * (k_ads / k_des) * p / (1 + (k_ads / k_des) * p)
Tyler Josephson (Nov 17 2021 at 19:12):
Broader goals would be to formalize less trivial derivations, such as those used in statistical mechanics.
Oliver Nash (Nov 17 2021 at 20:15):
I'd love to see a formal derivation of the Boltzmann equation.
Last updated: Sep 24 2022 at 19:12 UTC