You should use this repository to inspect the Lean 4 files that mathport has generated from mathlib3. Please run lake build first, to download a copy of the generated .olean files. After that, you should be able to open any of the .lean files under the Mathbin directory. These will use binported .oleans for the imports, and there is a synported .lean file for each file in mathlib3. Please expect many errors at this stage.

Although the Mathbin directory is committed in the repository, at this stage you should not attempt to make any changes on the master branch.

If you delete the Mathbin directory, then running lake build will download a new copy from the mathport release page. (It's probably safest to delete mathlib3-synport.tar.gz*, and probably lean_packages, too... This requires further automation.)

It's fine, however, to make branches containing "by-hand" edits, if you want to be able to link to diffs when reporting issues in mathport.