Zulip Chat Archive

Stream: Geographic locality

Topic: Newark, DE, USA


view this post on Zulip Alena Gusakov (Sep 05 2020 at 22:49):

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

view this post on Zulip Miles (Jan 18 2021 at 01:44):

Not too far away in Baltimore, MD

view this post on Zulip Tyler Josephson (Nov 16 2021 at 19:03):

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

view this post on Zulip Patrick Massot (Nov 16 2021 at 19:56):

Do you hope to explain chemistry to Lean?

view this post on Zulip 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.

view this post on Zulip Arthur Paulino (Nov 17 2021 at 16:51):

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

view this post on Zulip 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!?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Yaël Dillies (Nov 17 2021 at 17:21):

Kekule structures as well are out there.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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:

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!

view this post on Zulip Tyler Josephson (Nov 17 2021 at 19:12):

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

view this post on Zulip 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