Bare bones lean

Stream: new members

[Grigoriy Prokhrov]

Is it possible to start lean without any library, datatype or tactic and implement everything from scratch?

[Alex J. Best]

In lean3 adding prelude at the top of the file will not import the default init files, so you can work from a clean slate with very little included