Request for Paid Tutoring

Stream: general

[Michael Fishman]

Edit: I’ve found a tutor :D

Starting offer is $100 / hour, for 1 hour.

I'd like to hire a Lean tutor to help me express things in Lean. Tutoring would be remote, unless you're willing to meet in person in Boston.

Please let me know if you're interested!

First question - Discrete probabilities with named events and conditions

I want to express and manipulate discrete probability distributions.

For
$$
P(A, B) = P(A \mid B) \times P(B)
$$
I want the type of each term ($P(A, B), P(A \mid B), P(B)$) to express the _event_ and the _condition_. Eg. for $P(A \mid B)$, the event is $A$, and the condition is $B$.

I want to be able to fill in specific values for $A$ and $B$. Eg if I'm describing flower colors via $P(color \mid species)$, I want to be able to talk about specific colors and species, so that I could get generate a table like

|Color|Species|Probability|
|White|Orchid|0.5|
|Pink|Orchid|0.5|
|White|Pansy|0.4|
|Pink|Pansy|0.6|

My context

Why I'm interested in lean

As a software engineer and (dabbling) mathematician, I want to express my intent clearly and unambiguously.

What Lean I've learned so far

I've dabbled with lean on and off for a couple years. Went through a bit of Theorem Proving, a bit of Functional Programming, finished Number Game and most of Set Game. I spend more time than I'd like struggling with syntax, especially after a hiatus.