Introduction: Joseph McKinsey

Stream: new members

[Joseph McKinsey]

Hello, my name is Joseph McKinsey. My background is in applied math, and I mainly have been learning lean for fun. I still have lots of questions after going through "Mathematics in Lean". Where are existing issues filed for that? I would be interested in contributing minor fixes at least.

[Daniel Weber]

There is a github repository at https://github.com/leanprover-community/mathematics_in_lean

[Kabelo Moiloa]

Daniel Weber said:

There is a github repository at https://github.com/leanprover-community/mathematics_in_lean

To be more specific, looking at the Contributing section of the README.md of that repository, one has to file issues instead to this upstream repository.

[Joseph McKinsey]

Kabelo Moiloa said:

Daniel Weber said:

There is a github repository at https://github.com/leanprover-community/mathematics_in_lean

To be more specific, looking at the Contributing section of the README.md of that repository, one has to file issues instead to this upstream repository.

Thank you! I missed that somehow.