stream events

Stream: mathlib4

[Notification Bot]

Stream created by Scott Morrison.

[Kevin Cheung]

What kind of things could be discussed in this stream?

[Mario Carneiro]

Anything relating to mathlib porting, the mathlib4 repo, the interaction of lean 4 features and mathlib

[Daniel Fabian]

are you aware of the delaborator efforts by @Daniel Selsam , btw?

[Mario Carneiro]

The mathlib4 repo is introduced in this post. As mentioned there, the intent is for this to be a temporary from-scratch lean 4 repo, which will later be replaced by the results of porting. Tactics in particular are not slated for porting so they will have to be written from scratch anyway

[Mario Carneiro]

I will be manually porting a few more files but I expect not to get much further than data.nat.basic and data.list.basic, which covers most of the essentials for CS applications

[Mario Carneiro]

(To everyone who was pinged by the stream announcement: Sorry about that! Feel free to ignore.)

[Carter Schonwald]

Sounds fun!

[Mac]

Mario Carneiro said:

I will be manually porting a few more files but I expect not to get much further than data.nat.basic and data.list.basic, which covers most of the essentials for CS applications

If manual imports are the norm for now, is there some way we can organize who is doing what so that we don't reduplicate effort. For example, make a list of files (and/or sections of files) that would be noteworthy to port and have people comment what things they would like to take the reigns on.

It might be a nice way to get the community more into working with Lean 4 if there were some concrete goals to complete (that also have the reward of benefiting the community). I know it would interest me.

[Notification Bot]

Mario Carneiro changed the access permissions for this stream from Public to Web-public.

[Notification Bot]

Scott Morrison changed the description for this stream.

• Old description:

Porting mathlib to Lean 4

• New description:

The main mathematics library for Lean. Discuss future changes and contributions, ask questions about how it all works.

[Notification Bot]

Scott Morrison renamed stream mathlib4 to mathlib.

[Notification Bot]

Scott Morrison renamed stream mathlib to mathlib4.