First time user report

Stream: new members

[Joh-Tob Schäg]

Seldom can one approach a piece of software with fresh eyes. I was aware of lean before and used the z3 solver, MILP solvers, SAT solvers.
Today i decided to spend half a day to get a feel for this.
Here are somethings i encountered:

• There was no registration free channel to get in touch with the community.
• some zulip chanel descriptions are so long that i can't figure out to how to read it
• the new members channel could be split up, into seperate channels introduction and whatever else there is going on such as discussing beginner questions. I can't figure out how to read the entire channel description
• The distinction and incompatibilities between lean4 and lean3 is not clearly communicated. Now that i know that there is a differenrence i still can't easily tell whether stuff i find here https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html or https://github.com/leanprover-community/mathlib are meant to be used with lean3 or lean4 or both. A simple suggestion would be to color code resources, with distinct colors for 3 and 4 where ever possible but i see that that might be difficult for external sources
• It might be a good idea to have a bot send a message to new members which links all the reference neatly laid out by 3 vs 4 and purpose. This message could also contain encouraging words, suggestions how to get started.
• There is no lean3 channel which would contrast with an lean4 channel making it obvious both are active and maintained
• It is is not obvious where to ask questions as an user and especially as a new user
• the community, welcoming, thoughtful and thinking ahead however i imagine it must be frustrating to see the same questions come up again and again
• The linked tutorial material is frustratingly incomplete https://leanprover.github.io/reference/programming.html and not very apporachable if you have a specific question
• in my case i wanted to create a tupple of set, functions ... which have some basic property, define some trivial examples and see whether Lean recognizes that those do or do not conform with the defintions
  Here is my genuine attempt to do something:

import Mathlib.Data.Real.Basic -- hopefully imports the right thing
import Mathlib.set_theory.zfc.basic -- when things upper or lower case, it is not obvious to me how to find the correct import path for stuff

-- i went with a structure because the other examples of custom types were all inductive types which is not what i want, i think. Class might have also been interesting but the documentation went over my head and it didn't seem to be acknowledged in every documentation.
structure isosystem (T: Set Real) (U : Set T1) (X : Set T2) (Y : Set T3) (Uk : T.funs U) (phi : (Set.prod {(tp, tf) ∈ T × T | tf ≥ tp } Set.prod Uk X ).funs X ) (nu : (Set.prod T Set.prod X U).funs Y)

-- And input-state-output system is a hept-tupple of
-- a time set which is subset of the real numbers
-- an input set
-- a state set
-- an output set
-- a set of input signals which are functions T to U
-- a state transition function a larger and a smaller time, an input signal and a state to a new state
-- an output function which maps a time, a state and an input to an output

-- As you see i have no idea what i am doing.

-- In addition i would define some properties state of the transition function and when a system is linear or when a system is time invariant.

I didn't manage to accomplish that and you wouldn't help if you implemented that for me. It was an experiment to get a feel for lean and lean did not convince me that it could be useful for me in the near future or that i could meaningfully contribute somewhere. I'll keep an open mind about lean and i hope that these observation are interesting.

[Mario Carneiro]

There was no registration free channel to get in touch with the community.

You could send an email, but it's true that most methods will require you to do some kind of identification

some zulip chanel descriptions are so long that i can't figure out to how to read it

This is a zulip issue I suppose; you can see full channel descriptions at https://leanprover.zulipchat.com/#streams

the new members channel could be split up

We don't really have much of an introduction channel. Feel free to use the new members channel for either purpose

The distinction and incompatibilities between lean4 and lean3 is not clearly communicated

Right now, everything which doesn't explicitly say it is for lean 4 is for lean 3. Mathlib docs are lean 3, leanprover-community/mathlib is lean 3. Stuff about lean 4 has a 4 in the name somewhere

It might be a good idea to have a bot send a message to new members

I don't really think that's a good idea, as it would be the same message every time. You can't pin messages in zulip, so it is not well suited for this kind of information. For frequently asked questions, we usually use linkifiers which go to github wiki pages, e.g. #mwe, #backticks, #port-guide.

There is no lean3 channel which would contrast with an lean4 channel

All channels which don't have a 4 in the name are assumed to be about lean 3 by default. That includes #new members, #general , #maths which are the most heavily trafficked streams.

It is is not obvious where to ask questions as an user and especially as a new user

#new members

the community, welcoming, thoughtful and thinking ahead however i imagine it must be frustrating to see the same questions come up again and again

Sure, but you can't really "fix" this. If you write a bunch of documentation on everything then people will ask how to find things in the documentation. Personally I prefer just to respond to direct questions even if the questions have been asked before.

The linked tutorial material is frustratingly incomplete

True. Everything is a work in progress and even though there are a decent number of lean users it pales in comparison with even relatively obscure "regular" programming languages, because proofs are hard. This is a collaborative effort, so if you see something that you can help with please do.

[Mario Carneiro]

Regarding your final question: Note that the casing convention changed from lean 3 to lean 4. If you see everything in snake_case then it's probably lean 3 and if most things are in TitleCase then it is lean 4. import Mathlib.Data.Real.Basic looks like a line from a lean 4 file while import set_theory.zfc.basic is a lean 3 import (no Mathlib.). The corresponding lean 4 import line would be import Mathlib.SetTheory.ZFC.Basic

[Mario Carneiro]

you should use the lean 3 mathlib docs (docs#real) for info about lean 3, including the necessary imports, and the mathlib4 docs (docs4#Real) for lean 4 mathlib. In each case you will get information on imports, but you can construct the lean 4 name mechanically from the lean 3 name by putting the import in title case and prepending Mathlib..

[Joh-Tob Schäg]

Thank you for your detailed response. Your answer is a gold mine for insight. While your explanatation are sensible they are not necessarily obvious. By sending a message i meant a direct message not message in a public channel. There already is an welcome bot which greeted me with this:
@_Welcome Bot|100007 said:

Hello, and welcome to Zulip!

This is a private message from me, Welcome Bot. Here are some tips to get you started:

• Download our Desktop and mobile apps
• Customize your account and notifications on your Settings page
• Type ? to check out Zulip's keyboard shortcuts

The most important shortcut is r to reply.

Practice sending a few messages by replying to this conversation. If you're not into keyboards, that's okay too; clicking anywhere on this message will also do the trick!

Maybe that message can be customized? I don't use Zulip much.

[Mario Carneiro]

Unfortunately it cannot. I believe there is an open issue about this

[Mario Carneiro]

Here's my best guess at what you wanted to write for that code example:

import Mathlib.Data.Real.Basic

/-- An input-state-output system with input `U`, state `X` and output `Y` -/
structure ISOSystem (U X Y : Type _) :=
  /-- a time set which is subset of the real numbers -/
  T : Set Real
  /-- a set of input signals which are functions T to U -/
  Uk : Set (T → U)
  /-- a state transition function a larger and a smaller time, an input signal and a state to a new state -/
  phi : ∀ tp tf : T, tp ≤ tf → Uk → X → X
  /-- an output function which maps a time, a state and an input to an output -/
  nu : T → X → U → Y