← Back to context Comment by mejutoco 2 days ago I dont think mathlib is mandatory to use lean. 4 comments mejutoco Reply empath75 2 days ago It isn’t but the borrow checker has a formal proof that does need mathlib. mejutoco 17 hours ago > having a mathlib dependency just to build a programming language is a big ask for people.This is an implementation choice you did when implementing your programming language, if I understand correctly.I thought of it because writing some lean lang I also had the option of adding Mathlib or keep it "bare". ndriscoll 2 days ago You can define whatever you actually rely on as an axiom. thaumasiotes 2 days ago Publishing the proof is good, but why do you need it to build the language?You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.
empath75 2 days ago It isn’t but the borrow checker has a formal proof that does need mathlib. mejutoco 17 hours ago > having a mathlib dependency just to build a programming language is a big ask for people.This is an implementation choice you did when implementing your programming language, if I understand correctly.I thought of it because writing some lean lang I also had the option of adding Mathlib or keep it "bare". ndriscoll 2 days ago You can define whatever you actually rely on as an axiom. thaumasiotes 2 days ago Publishing the proof is good, but why do you need it to build the language?You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.
mejutoco 17 hours ago > having a mathlib dependency just to build a programming language is a big ask for people.This is an implementation choice you did when implementing your programming language, if I understand correctly.I thought of it because writing some lean lang I also had the option of adding Mathlib or keep it "bare".
thaumasiotes 2 days ago Publishing the proof is good, but why do you need it to build the language?You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.
It isn’t but the borrow checker has a formal proof that does need mathlib.
> having a mathlib dependency just to build a programming language is a big ask for people.
This is an implementation choice you did when implementing your programming language, if I understand correctly.
I thought of it because writing some lean lang I also had the option of adding Mathlib or keep it "bare".
You can define whatever you actually rely on as an axiom.
Publishing the proof is good, but why do you need it to build the language?
You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.