Zulip Chat Archive

Stream: new members

Topic: Hello!


view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:23):

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?

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:25):

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

view this post on Zulip Kevin Buzzard (Nov 06 2020 at 08:29):

Don't unfold anything, use the interface.

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:35):

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!

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:36):

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.

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:42):

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.

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:43):

No repl.

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:43):

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

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:44):

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.)

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:44):

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

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:44):

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

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:45):

when I have to use vscode

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:45):

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

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:45):

Basic advice is to never use vim plugin undo.

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:45):

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

view this post on Zulip Patrick Massot (Nov 06 2020 at 08:46):

Have a good night!

view this post on Zulip Abhishek Cherath (Nov 06 2020 at 08:46):

gn

view this post on Zulip Thomas Powell (Feb 03 2021 at 17:39):

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!


Last updated: May 12 2021 at 23:13 UTC