Hello!

Stream: new members

[Abhishek Cherath]

Heya, I'm Abhishek Cherath, I'm a 3rd year at Stony Brook University. I just finished the natural number game, and it was fun. I'm going to attempt to do my continuity homework using lean next, any advice?

[Patrick Massot]

Did you followed installation instructions? Then my advice is to go through the tutorials project which contains lots of elementary continuity stuff.

[Kevin Buzzard]

Don't unfold anything, use the interface.

[Abhishek Cherath]

Patrick Massot said:

Did you followed installation instructions? Then my advice is to go through the tutorials project which contains lots of elementary continuity stuff.

yep just got it running (had some weird pipx issues, but deleting and reinstalling seemed to fix it), and that seems like exactly what I need to look at, thank you!

[Patrick Massot]

Note that the installation instructions directed you to https://leanprover-community.github.io/install/project.html which contains instructions to install the tutorials project without pain.

[Abhishek Cherath]

Patrick Massot said:

Note that the installation instructions directed you to https://leanprover-community.github.io/install/project.html which contains instructions to install the tutorials project without pain.

yep! got it up. also, just to make sure, there's no lean repl ala ipython or something right? I ask because I mostly only use vim, and while I don't mind vscode I wouldn't mind NOT using it either.

[Patrick Massot]

No repl.

[Patrick Massot]

And, very sadly, using anything but VSCode is asking for a lot of pain, and would make it much harder to get help here.

[Abhishek Cherath]

Patrick Massot said:

And, very sadly, using anything but VSCode is asking for a lot of pain, and would make it much harder to get help here.

yea I figured. Like I said, no issue (But a potential future contribution from me, hopefully.)

[Patrick Massot]

Note that VSCode has several extension pretending to bring vim emulation, and many people here (including me) use them. But they are definitely buggy.

[Abhishek Cherath]

Patrick Massot said:

Note that VSCode has several extension pretending to bring vim emulation, and many people here (including me) use them. But they are definitely buggy.

https://github.com/asvetliakov/vscode-neovim this is what I use

[Abhishek Cherath]

when I have to use vscode

[Patrick Massot]

The main big bug is unpredictable undo. VSCode undo list and vim plugin undo list live separate lives and fight each other.

[Patrick Massot]

Basic advice is to never use vim plugin undo.

[Abhishek Cherath]

alright I'll be sleeping now (345 AM here hehe), but I'll get started tom, thanks for the help!

[Patrick Massot]

Have a good night!

[Abhishek Cherath]

gn

[Thomas Powell]

Hi, just wanted to introduce myself quickly: I'm Thomas Powell and I lecture computer science at Bath, though my research interests are primarily mathematical and centered around applications of proof theory in mathematics (also known as "proof mining").

I've been meaning to try my hand at formalisation for a while now, and there's a ton of stuff from my area which would probably make for interesting formalisation projects, including things like proof interpretations, higher-order computability theory and relevant stuff from computable analysis, like rates of convergence.

I also have an ulterior motive, which is to experience the theorem prover learning curve myself, with an eye on getting my future students interested, and potentially setting them up with undergraduate projects based the formalisation of topics from computer science. But before any of that happens, I'm going to need to ask a ton of stupid questions myself!

[Paul Reichert]

Hello everyone, my name is Paul and I am currently writing my Master's thesis in Karlsruhe, Germany, in the field of convex geometry. I'm currently trying to formalize a subtle chapter using Lean, sorrying classical results from Brunn-Minkowski theory that are still missing in mathlib, but I plan to implement and contribute some of them later to mathlib. I must say that the library is pretty impressive and usable at this point.

[Patrick Massot]

Welcome! There may be more Brunn-Minkowski stuff buried in old pull-requests. Maybe ask @Alex J. Best

[Alex J. Best]

I don't think I ever worked on Brunn-Minkowski, only Minkowskis convex body theorem, of course that theorem or some of it's lemmas may also be useful in places, and I know @Yaël Dillies and I have been thinking about modernizing that work recently.

[Yaël Dillies]

Hey! Indeed #2819 is being bumped and cleaned up (slowly, because I do not yet know my way around measure theory library). And incidentally I will be working on Brunn-Minkowski once my summer internship is over.

[Johan Commelin]

@Yaël Dillies Maybe you should start maintaining a public list of all Lean projects... you seem to be working on everything :open_mouth: :stuck_out_tongue_wink:

[Johan Commelin]

(Also, it would help check whether you are blocking others from working on certain topics if something you've started working on slipped down your priority queue.)

[Kevin Buzzard]

Yeah, you reopened #4956 nearly a year ago and it's clogging up my "view all PRs" page ;-) (not that I actually care)

[Yaël Dillies]

Sorry Kevin! :grinning:

[Yaël Dillies]

Yeah, feel free to do Brunn-Minkowski if you have time before I do (namely, october).

[Paul Reichert]

Fine. I plan to try as soon as I have verified my proof and get back to you all when or if I start, @Yaël Dillies

[Brendon James Thomson]

Hello, I'm a Concordia University (Montreal) Pure & Applied Mathematics undergraduate student. I've played and completed the Natural Number Game and I've also done the tutorial as well. I wanted to try my shot at the theorem that all groups of order p^2, where p is a prime, are commutative, but the task seems daunting at the moment.

I've given a look at the Contributing section (https://leanprover-community.github.io/contribute/index.html) but I can't seem to get over the hump, I just need a nudge in the right direction!

Any help would be appreciated, preferably something step-by-step.

[Kevin Buzzard]

Just to let you know, this was recently PRed to mathlib. I'm not clear what you're asking. You want to know how to prove the theorem or how to get something into mathlib?

[Brendon James Thomson]

Does that mean the theorem was already contributed? I would like to know how to get something into mathlib (:

[Thomas Browning]

The theorem has already been contributed: docs#is_p_group.comm_group_of_card_eq_prime_sq
The first step to contributing is leanproject get -b mathlib:my_branch_name in the terminal. And then you can start editing mathlib files.

[Mauricio Collares]

The docstrings seem swapped, by the way

[Thomas Browning]

Yeah, just noticed. I'm making a PR to fix it right now :)

[Brendon James Thomson]

"The theorem has already been contributed" - not a problem (: