Newark, DE, USA

Stream: Geographic locality

[Alena Gusakov]

University of Delaware graduate in math and computer science here! Just realized this stream existed lol

[Miles]

Not too far away in Baltimore, MD

[Tyler Josephson]

Hey! I'm in Baltimore, too. Assistant prof in Chemical Engineering. https://cbee.umbc.edu/josephson/

[Patrick Massot]

Do you hope to explain chemistry to Lean?

[Tyler Josephson]

Yep! I just started training an undergrad Chemical Engineering student, who has been enjoying the Natural Number Game.

[Arthur Paulino]

Interesting! I'm curious to see what/how branches of chemistry can be formalized!

[Julian Berman]

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]

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]

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]

Kekule structures as well are out there.

[Yakov Pechersky]

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]

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]

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:

Given:
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)

Prove:
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)
Done!

[Tyler Josephson]

Broader goals would be to formalize less trivial derivations, such as those used in statistical mechanics.

[Oliver Nash]

I'd love to see a formal derivation of the Boltzmann equation.