# Zulip Chat Archive

## Stream: general

### Topic: Intuitionistic Type Theory Proofs

#### Billy Price (Apr 15 2020 at 13:44):

Hi there,

I'm doing a project on topos theory and proof-assistants, and I would like to write some proofs about intuitionistic type theory as presented in Lambek and Scott "Introduction to Higher Order Logic", specifically I'm proving that its associated category is a topos. The sequent-tree-proofs are laborious to organise and write out by hand. Would Lean be an appropriate tool for this?

I essentially want to define Term's inductively, and then create and work with sequents of the form "p |--_X q", where |--_X is entailment with a subscript set X of variables, and p,q are Terms with free variables all in X. I am imagining then implementing the rules of deduction as axioms like this, "axiom rule : A -> B" where A and B are entailment expressions as before.

I am unsure how I should marry Lean's existing type theory with the one I'm modelling. Should I endeavour to completely separate them? For example, one rule is "(r|--_X p & q) iff (r|--_X p) and (r|--_X q)", in which case I imagine I should write my own conjuction for the use of "&" and use the existing "and" and "iff" in Lean's library.

#### Reid Barton (Apr 15 2020 at 13:49):

This sounds like approximately the right approach except that, instead of using `axiom`

, make "p |--_X q" an inductive Prop with the rules of deduction as constructors.

#### Reid Barton (Apr 15 2020 at 13:53):

Or maybe a type rather than a prop depending on what you want to do with it

#### Patrick Massot (Apr 15 2020 at 13:56):

https://flypitch.github.io/ is probably useful as an example of embedding other theories into Lean.

#### Billy Price (Apr 15 2020 at 13:57):

Something like this? I'm still new to lean and I'm 100% certain this is wrong.

"inductive entails (X : set) (p : Term) (q: Term)

| self_entail : entails X p p

"

#### Kevin Buzzard (Apr 15 2020 at 13:58):

` ```lean `

at the top of your code and ` ``` `

at the bottom to quote it with syntax highlighting

#### Andrew Ashworth (Apr 15 2020 at 13:59):

On top of Flypitch, there is also https://softwarefoundations.cis.upenn.edu/plf-current/Types.html#lab174, which shows something related but not quite (also it's in Coq, so you have to translate syntax)

#### Billy Price (Apr 15 2020 at 14:03):

Patrick Massot said:

https://flypitch.github.io/ is probably useful as an example of embedding other theories into Lean.

Is their use of the unicode \entails a defined notation or is that already part of lean?

#### Patrick Massot (Apr 15 2020 at 14:11):

@Floris van Doorn @Jesse Michael Han

#### Jesse Michael Han (Apr 15 2020 at 17:44):

we define our own notion of provability for first-order logic, see fol.lean in the Flypitch repo

#### Floris van Doorn (Apr 16 2020 at 05:22):

Provability is defined in the repository:

inductive prf : set (formula L) → formula L → Type u | axm {Γ A} (h : A ∈ Γ) : prf Γ A | impI {Γ : set $ formula L} {A B} (h : prf (insert A Γ) B) : prf Γ (A ⟹ B) | impE {Γ} (A) {B} (h₁ : prf Γ (A ⟹ B)) (h₂ : prf Γ A) : prf Γ B | falsumE {Γ : set $ formula L} {A} (h : prf (insert ∼A Γ) ⊥) : prf Γ A | allI {Γ A} (h : prf (lift_formula1 '' Γ) A) : prf Γ (∀' A) | allE₂ {Γ} A t (h : prf Γ (∀' A)) : prf Γ (A[t // 0]) | ref (Γ t) : prf Γ (t ≃ t) | subst₂ {Γ} (s t f) (h₁ : prf Γ (s ≃ t)) (h₂ : prf Γ (f[s // 0])) : prf Γ (f[t // 0])

https://github.com/flypitch/flypitch/blob/master/src/fol.lean#L816

This is all done on top of our internal definition of formula of first-order logic.

Here ` prf Γ A`

stands for `Γ ⊢ A`

. So for example `impE`

states that if `Γ ⊢ A ⟹ B`

and `Γ ⊢ A`

then `Γ ⊢ B`

. Some of the other rules are a bit more tricky to decipher, this is because we're using de Bruijn indices for formulas. More details can be found in the two papers we wrote about it: https://flypitch.github.io/papers/

#### Billy Price (Apr 25 2020 at 03:07):

I'm trying to write the inductive definition of a Formula in my type theory, in which every Type has a powerset type. One of the Formulas is of the form "a \in \alpha", where A is a type, a : A, and \alpha : PA. However Lean is not happy when I try to define this constructor on the last line - "universe level of type_of(arg #1) of 'TypeTheory.Formula.elem' is too big for the corresponding inductive datatype"

structure PowerSet (A : Type) : Type inductive Formula : Type | var : ℕ → Formula | top : Formula | bot : Formula | and : Formula → Formula → Formula | or : Formula → Formula → Formula | imp : Formula → Formula → Formula | elem {A : Type} : A → (PowerSet A) → Formula

I imagine its because I've defined a lot of things to be of type `Type`

, but I don't really understand where things should live. Those things being: the types of my theory (instances of A in my code above), the powersets of those types (same level as normal types?), and Formulas.

#### Donald Sebastian Leung (Apr 25 2020 at 03:09):

Perhaps try adding the type parameter `A`

to `Formula`

itself, i.e. `inductive Formula (A : Type) : Type`

#### Billy Price (Apr 25 2020 at 03:13):

Okay cool, I'd like to know why that worked, but also it seems like now every constructor of Formula now depends on this type, which I don't think I want.

#### Mario Carneiro (Apr 25 2020 at 04:01):

More precisely, this makes it so that there is only one type over which `elem`

can work

#### Mario Carneiro (Apr 25 2020 at 04:02):

You can make `Formula`

live in `Type 1`

and then it will work, but the better question is what you intend to do with an uncountable number of formulas

#### Mario Carneiro (Apr 25 2020 at 04:02):

I think you need some constraints on what types are supposed to exist in your type theory

#### Billy Price (Apr 25 2020 at 04:33):

Why would it be uncountable? Surely the fact that it's defined inductively only gives me countably many?

#### Kenny Lau (Apr 25 2020 at 04:35):

`elem x`

is different for each `x : Type`

#### Kenny Lau (Apr 25 2020 at 04:35):

what does `PowerSet A`

do?

#### Kenny Lau (Apr 25 2020 at 04:36):

it has no constructor so there can be no instances of it...

#### Mario Carneiro (Apr 25 2020 at 04:36):

actually it's a `structure`

so there is one for each `A`

#### Billy Price (Apr 25 2020 at 04:37):

I am ambivalent to what PowerSet A is, just that it's also a type in the same way that A is

#### Mario Carneiro (Apr 25 2020 at 04:37):

but the problem is that `A`

can be anything

#### Kenny Lau (Apr 25 2020 at 04:37):

I claim that `PowerSet A -> false`

for all `A`

#### Mario Carneiro (Apr 25 2020 at 04:38):

that's false, `PowerSet A ~= unit`

#### Kenny Lau (Apr 25 2020 at 04:38):

I don't understand structures

#### Billy Price (Apr 25 2020 at 04:39):

Yeah okay, well here's my updated attempt (doesn't compile)

inductive type : Type 1 | prod : type → type → type | pow : type → type inductive Formula : Type 1 | top : Formula | bot : Formula | and : Formula → Formula → Formula | or : Formula → Formula → Formula | imp : Formula → Formula → Formula | elem {A : type} : A → (type.pow A) → Formula

#### Mario Carneiro (Apr 25 2020 at 04:39):

@Billy Price What I think you want is an inductive type declaring the valid types of your theory. At minimum, it should include `PowerSet`

and some fixed collection of base types

#### Kenny Lau (Apr 25 2020 at 04:39):

PowerSet.rec : Π {A : Type} {C : PowerSet A → Sort u_1}, C PowerSet.mk → Π (n : PowerSet A), C n

#### Kenny Lau (Apr 25 2020 at 04:39):

now I can claim that `type -> false`

#### Billy Price (Apr 25 2020 at 04:40):

This is the Type theory I am trying to model in Lean. http://therisingsea.org/notes/ch2018-lecture9.pdf

#### Mario Carneiro (Apr 25 2020 at 04:40):

@Kenny Lau A structure is like an inductive type with one constructor and many arguments. So it is basically a product of all the fields, and the 0-ary case is unit

#### Kenny Lau (Apr 25 2020 at 04:40):

structure PowerSet (A : Type) : Type inductive Formula : Type 1 | var : ℕ → Formula | top : Formula | bot : Formula | and : Formula → Formula → Formula | or : Formula → Formula → Formula | imp : Formula → Formula → Formula | elem {A : Type} : A → (PowerSet A) → Formula

#### Kenny Lau (Apr 25 2020 at 04:40):

I'm not sure if this is the intended interpretation

#### Kenny Lau (Apr 25 2020 at 04:41):

@Mario Carneiro I see

#### Mario Carneiro (Apr 25 2020 at 04:42):

Here's an easy fix:

inductive type : Type | prod : type → type → type | pow : type → type inductive Formula : Type | top : Formula | bot : Formula | and : Formula → Formula → Formula | or : Formula → Formula → Formula | imp : Formula → Formula → Formula | elem {A : type} : ℕ → ℕ → Formula

#### Mario Carneiro (Apr 25 2020 at 04:42):

The problem is that you don't have a grammar of terms that can inhabit a type

#### Mario Carneiro (Apr 25 2020 at 04:42):

here I'm just assuming they are numbered variables, and the type checking is separate

#### Mario Carneiro (Apr 25 2020 at 04:43):

Also, `type`

is empty

#### Mario Carneiro (Apr 25 2020 at 04:45):

Here's a more well typed version

inductive type : Type | prod : type → type → type | pow : type → type def term : type → Type | (type.prod a b) := term a × term b | (type.pow a) := term a → Prop inductive Formula : Type | top : Formula | bot : Formula | and : Formula → Formula → Formula | or : Formula → Formula → Formula | imp : Formula → Formula → Formula | elem {A : type} : term A → term (type.pow A) → Formula

but it's still not good because there are too many elements of `term (type.pow a)`

#### Billy Price (Apr 25 2020 at 04:46):

Yeah I need to add Unit and Omega, where Omega is interpreted as the type of propositions. At the moment I was modelling Omega with Formula, without explicitly calling it a `type`

, maybe I should try that

#### Kenny Lau (Apr 25 2020 at 04:47):

I **don't** think the intended meaning is "1 is a Type, Ω is a Type, AxB is a type for each A and B, PA is a type for each A, **and this is all there is to it**"

#### Kenny Lau (Apr 25 2020 at 04:47):

i.e. I don't agree with the use of `inductive`

#### Mario Carneiro (Apr 25 2020 at 04:47):

The problem is that this is going to turn into an inductive-recursive type if you aren't careful

#### Mario Carneiro (Apr 25 2020 at 04:47):

because the definition of `term`

depends on `formula`

and vice versa

#### Billy Price (Apr 25 2020 at 04:51):

@Kenny Lau Would it not be possible to inject the semantics of each of these types later on?

#### Mario Carneiro (Apr 25 2020 at 04:52):

When I look at the lecture notes you linked, I see a description of a structure, a system of constraints that defines a "type system", not an inductive type enumerating all possible terms

#### Kenny Lau (Apr 25 2020 at 04:53):

inductive type : Type | one | Omega | prod (A B : type) | pow (A : type) inductive term : type → Type | prod : Π A B : type, term A → term B → term (type.prod A B) | elem : Π A : type, term A → term (type.pow A) → term type.Omega -- what is b3? | and : term type.Omega → term type.Omega → term type.Omega | or : term type.Omega → term type.Omega → term type.Omega | imp : term type.Omega → term type.Omega → term type.Omega -- what is b5??

#### Kenny Lau (Apr 25 2020 at 04:53):

@Mario Carneiro and then I looked deeper, and they defined "Pure type theory" to be basically the inductive thing

#### Kenny Lau (Apr 25 2020 at 04:53):

I'm not sure how to formalize "a variable x of type A"

#### Kenny Lau (Apr 25 2020 at 04:53):

which is required in b3 and b5

#### Kenny Lau (Apr 25 2020 at 04:53):

but here's b2 formalized @Billy Price

#### Mario Carneiro (Apr 25 2020 at 04:55):

A variable of type A would be a constructor `| var {A : type} : nat -> term A`

#### Billy Price (Apr 25 2020 at 04:56):

Awesome, thanks. For the variables, I just need them to act such that I can substitute terms of the `type`

that the variable is associated to.

#### Kenny Lau (Apr 25 2020 at 04:56):

inductive type : Type | one | Omega | prod (A B : type) | pow (A : type) inductive term : type → Type | prod : Π A B : type, term A → term B → term (type.prod A B) | elem : Π A : type, term A → term (type.pow A) → term type.Omega | sep : Π A : type, term type.Omega → ℕ → term (type.pow A) | and : term type.Omega → term type.Omega → term type.Omega | or : term type.Omega → term type.Omega → term type.Omega | imp : term type.Omega → term type.Omega → term type.Omega | all : Π A : type, term type.Omega → ℕ → term type.Omega | ex : Π A : type, term type.Omega → ℕ → term type.Omega

#### Kenny Lau (Apr 25 2020 at 04:56):

how does this look

#### Mario Carneiro (Apr 25 2020 at 04:57):

If you use de bruijn variables you don't need the index on `sep`

,`all`

,`ex`

#### Mario Carneiro (Apr 25 2020 at 04:58):

and you are still missing `var`

#### Mario Carneiro (Apr 25 2020 at 04:59):

also `star`

,`true`

,`false`

#### Kenny Lau (Apr 25 2020 at 05:01):

inductive type : Type | one | Omega | prod (A B : type) | pow (A : type) inductive term : type → Type | var : Π A : type, ℕ → term A | star : term type.one | true : term type.Omega | false : term type.Omega | prod : Π A B : type, term A → term B → term (type.prod A B) | elem : Π A : type, term A → term (type.pow A) → term type.Omega | sep : Π A : type, term type.Omega → ℕ → term (type.pow A) | and : term type.Omega → term type.Omega → term type.Omega | or : term type.Omega → term type.Omega → term type.Omega | imp : term type.Omega → term type.Omega → term type.Omega | all : Π A : type, term type.Omega → ℕ → term type.Omega | ex : Π A : type, term type.Omega → ℕ → term type.Omega

#### Kenny Lau (Apr 25 2020 at 05:02):

what do you mean by use de Bruijn variables?

#### Mario Carneiro (Apr 25 2020 at 05:02):

that is, binders are defined so that all variable numbers shift up by one and variable number 0 becomes the newly introduced variable

#### Billy Price (Apr 25 2020 at 05:03):

same question from me, and I'm also curious how in Lean I could go about "actually substituting terms" in either of these cases.

#### Mario Carneiro (Apr 25 2020 at 05:03):

You have to define `subst`

by recursion

#### Mario Carneiro (Apr 25 2020 at 05:04):

This is as opposed to named variables where you say "variable k is bound now" and all other variable names stay the same (and variable k outside the binder is not accessible from inside the binder)

#### Mario Carneiro (Apr 25 2020 at 05:04):

here it makes just as much sense to use `string`

as `nat`

for the names of variables, but you need to know that there is a way to get fresh variables when you need them

#### Kenny Lau (Apr 25 2020 at 05:04):

inductive type : Type | one | Omega | prod (A B : type) | pow (A : type) inductive term : type → Type | var : Π A : type, ℕ → term A | star : term type.one | true : term type.Omega | false : term type.Omega | prod : Π A B : type, term A → term B → term (type.prod A B) | elem : Π A : type, term A → term (type.pow A) → term type.Omega | sep : Π A : type, term type.Omega → ℕ → term (type.pow A) | and : term type.Omega → term type.Omega → term type.Omega | or : term type.Omega → term type.Omega → term type.Omega | imp : term type.Omega → term type.Omega → term type.Omega | all : Π A : type, term type.Omega → ℕ → term type.Omega | ex : Π A : type, term type.Omega → ℕ → term type.Omega def FV : Π {A : type}, term A → finset ℕ | _ (term.var A n) := {n} | _ term.star := ∅ | _ term.true := ∅ | _ term.false := ∅ | _ (term.prod A B a b) := FV a ∪ FV b | _ (term.elem A a α) := FV a ∪ FV α | _ (term.sep A a n) := (FV a).erase n | _ (term.and p q) := FV p ∪ FV q | _ (term.or p q) := FV p ∪ FV q | _ (term.imp p q) := FV p ∪ FV q | _ (term.all A φ n) := (FV φ).erase n | _ (term.ex A φ n) := (FV φ).erase n

#### Mario Carneiro (Apr 25 2020 at 05:05):

yep

#### Kenny Lau (Apr 25 2020 at 05:05):

this doesn't use de Bruijn though

#### Mario Carneiro (Apr 25 2020 at 05:05):

no

#### Mario Carneiro (Apr 25 2020 at 05:05):

this is the named variables approach

#### Mario Carneiro (Apr 25 2020 at 05:05):

The other major issue with named variables is that alpha equivalence is a thing

#### Kenny Lau (Apr 25 2020 at 05:06):

do I just remove the N if I want to use de Bruijn?

#### Kenny Lau (Apr 25 2020 at 05:06):

inductive type : Type | one | Omega | prod (A B : type) | pow (A : type) inductive term : type → Type | var : Π A : type, ℕ → term A | star : term type.one | true : term type.Omega | false : term type.Omega | prod : Π A B : type, term A → term B → term (type.prod A B) | elem : Π A : type, term A → term (type.pow A) → term type.Omega | sep : Π A : type, term type.Omega → term (type.pow A) | and : term type.Omega → term type.Omega → term type.Omega | or : term type.Omega → term type.Omega → term type.Omega | imp : term type.Omega → term type.Omega → term type.Omega | all : Π A : type, term type.Omega → term type.Omega | ex : Π A : type, term type.Omega → term type.Omega

#### Kenny Lau (Apr 25 2020 at 05:06):

like this?

#### Mario Carneiro (Apr 25 2020 at 05:06):

It affects `FV`

and `subst`

#### Mario Carneiro (Apr 25 2020 at 05:06):

but yes, in the definition itself that's all

#### Mario Carneiro (Apr 25 2020 at 05:07):

you need operations like `lift`

too

#### Kenny Lau (Apr 25 2020 at 05:07):

what's the signature of `lift`

?

#### Mario Carneiro (Apr 25 2020 at 05:08):

`lift' : nat -> nat -> term A -> term A`

is such that `lift' k n`

changes `var i`

to `var i`

if `i < k`

and `var (i+n)`

otherwise

#### Kenny Lau (Apr 25 2020 at 05:08):

def FV : Π {A : type}, term A → finset ℕ | _ (term.var A n) := {n} | _ term.star := ∅ | _ term.true := ∅ | _ term.false := ∅ | _ (term.prod A B a b) := FV a ∪ FV b | _ (term.elem A a α) := FV a ∪ FV α | _ (term.sep A a) := ((FV a).erase 0).image nat.pred | _ (term.and p q) := FV p ∪ FV q | _ (term.or p q) := FV p ∪ FV q | _ (term.imp p q) := FV p ∪ FV q | _ (term.all A φ) := ((FV φ).erase 0).image nat.pred | _ (term.ex A φ) := ((FV φ).erase 0).image nat.pred

#### Kenny Lau (Apr 25 2020 at 05:08):

is this right?

#### Mario Carneiro (Apr 25 2020 at 05:09):

You should consult the flypitch project, they worked this all out

#### Mario Carneiro (Apr 25 2020 at 05:09):

https://github.com/flypitch/flypitch/blob/master/src/fol.lean#L252-L255

#### Mario Carneiro (Apr 25 2020 at 05:10):

see also https://github.com/flypitch/flypitch/blob/master/src/fol.lean#L610-L616 for how binders affect things

#### Billy Price (Apr 25 2020 at 05:10):

Yeah I've been consulting that as much as possible, but I found it a little difficult to translate to my theory, thank you both for guiding me.

#### Mario Carneiro (Apr 25 2020 at 05:11):

I think in flypitch they never bothered to define FV, because in de bruijn world it is just as good to say "all variables are less than n"

#### Billy Price (Apr 25 2020 at 05:12):

So if I use de bruijn indices, have I completely avoided the need for alpha equivalence?

#### Mario Carneiro (Apr 25 2020 at 05:12):

yes, that's their secret weapon

#### Billy Price (Apr 25 2020 at 05:14):

I would imagine this would need to be hardwired into how `all`

, `ex`

and `sep`

are defined, but it seems like you said otherwise above?

#### Mario Carneiro (Apr 25 2020 at 05:15):

Well, it's a type theory, so there isn't much of a "definition" of all,ex,sep

#### Billy Price (Apr 25 2020 at 05:15):

(deleted)

#### Mario Carneiro (Apr 25 2020 at 05:15):

they are just primitive constants, and so far as that goes you just get to remove the `x`

#### Mario Carneiro (Apr 25 2020 at 05:15):

The actual content comes in when you write down the rules of the type theory

#### Billy Price (Apr 25 2020 at 05:19):

So if I construct a term with var 7 in it, I have decided at that moment that 7 is bound to the 7th binder "out" from the appearance of 7?

#### Billy Price (Apr 25 2020 at 05:19):

And the lifting is to change that number in case I want to bind it to a different "level" binder?

#### Mario Carneiro (Apr 25 2020 at 05:20):

yes, although the convention is that if there are fewer than 7 binders then it is a free variable and you haven't decided yet what to bind it to

#### Mario Carneiro (Apr 25 2020 at 05:20):

Right, you need lifting when you want to move an expression from an outer context under a binder without accidentally capturing the new variable

#### Mario Carneiro (Apr 25 2020 at 05:23):

I find it helpful to think of the expression like `x : nat, y : nat |- x + y`

carrying its context with it, where here `x`

is var 1 and `y`

is var 0, and lift corresponds to moving this expression into a new context `x : nat, y : nat, z : nat |- x + y`

where now `x`

is var 2 and `y`

is var 1

#### Billy Price (Apr 25 2020 at 05:25):

Thats makes it seem that you'd only ever need to lift by 1?

#### Mario Carneiro (Apr 25 2020 at 05:26):

The general lift comes up when you define lift by recursion

#### Billy Price (Apr 25 2020 at 05:26):

Ah okay

#### Billy Price (Apr 25 2020 at 05:28):

Do I need to use lift again (with negative n?) when you want to substitute a variable for a term?

#### Mario Carneiro (Apr 25 2020 at 05:29):

You use `subst : term A -> term A -> term A`

, which has the effect of substituting variable 0 for t and lowering all other variables by 1

#### Billy Price (Apr 25 2020 at 05:29):

So I'm limited to only substituting variable 0?

#### Mario Carneiro (Apr 25 2020 at 05:30):

The general version of this also has to include a lift component, where variable k gets substituted, variables above k get reduced by 1, and variables below k stay the same

#### Mario Carneiro (Apr 25 2020 at 05:30):

You should only ever have to substitute variable 0

#### Mario Carneiro (Apr 25 2020 at 05:30):

because of the way the binders are set up

#### Billy Price (Apr 25 2020 at 05:31):

I'm not sure I follow, you just said I could substitute for general variable k

#### Mario Carneiro (Apr 25 2020 at 05:32):

Like with lift, where you only actually need to lift by 1 but other lifts come up in the inductive definition, in subst you only need to substitute variable 0 but as you go through the binders it stops being variable 0

#### Mario Carneiro (Apr 25 2020 at 05:34):

you should look at `subst_realize`

, `subst_term`

and `subst_formula`

in flypitch to see how it is done

#### Billy Price (Apr 25 2020 at 05:35):

Cheers, will do

#### Billy Price (Apr 25 2020 at 05:38):

Thanks again for your help :)

#### Patrick Massot (Apr 25 2020 at 09:38):

I think we really need to create a new stream here. We have a math string so that people who are not interested in maths can avoid math messages. I don't know how to call that new stream, and maybe we need more than one, but I would really like to avoid seeing all those discussions about embedding other type theories or ZFC into Lean, and all those discussions about proving programs. I'm very happy that other people find this interesting and use Lean for this purpose. But many people around here have zero interest in those things and can't contribute any useful comment. This is a pretty high traffic chat so we need order. We can't put such specialized discussion in the general stream I also guess some people would actually ask more computer science questions if we had a dedicated stream.

#### Donald Sebastian Leung (Apr 25 2020 at 09:50):

Perhaps we could create a stream "computer science"?

Or should we name it "type theory" / "PL theory"?

#### Patrick Massot (Apr 25 2020 at 09:52):

And I just had my standard half second of utter confusion about why piecewise linear theory enters this discussion. I proves once again we really need to sort things a bit.

#### Kenny Lau (Apr 25 2020 at 09:52):

Computer Science, Logic, Program Verification

#### Patrick Massot (Apr 25 2020 at 09:53):

I think we need to separate CS/logic from Program verification, but people who understand those things should tell us

#### Billy Price (Apr 25 2020 at 10:51):

My apologies, I'm new to Zulip Chat so I wasn't sure where else to put this topic.

#### Kevin Buzzard (Apr 25 2020 at 11:08):

It's a fine place to put it :-) But it's certainly true that for people like Patrick and me, we can understand a lot of the chat in general but just don't have the CS background to follow stuff like this because we're mathematicians

#### Patrick Massot (Apr 25 2020 at 11:21):

@Billy Price there is *no reason* to apologize. I'm exactly pointing out that you had no choice, and this is a problem.

#### Billy Price (Apr 25 2020 at 11:23):

Okay no worries :)

#### Patrick Massot (Apr 25 2020 at 11:29):

Let me emphasize: when I write I'm happy that people work on this topic, use Lean for this, and ask questions about it, I *really* mean it. And I'm also super happy there are so many messages on this chat. But we simply need ways to filter out stuff. There is no hierarchy involved here, only a lot of people with a lot of different priorities, and only 24 hours a day.

#### Billy Price (Apr 28 2020 at 12:56):

I haven't seen any more discussion of this. Who's decision is it regarding making new streams?

#### Patrick Massot (Apr 28 2020 at 12:57):

Anyone can create one. But it would be natural for @Mario Carneiro to decide something here

#### Mario Carneiro (Apr 28 2020 at 12:57):

I guess we can do a type theory stream, CS is too broad

#### Mario Carneiro (Apr 28 2020 at 12:58):

Logic is also a bit unclear

#### Billy Price (Apr 28 2020 at 12:58):

Just to clarify, we're talking about making a stream on the same level as "announce", "general", "maths" etc? Do you call the ones inside those substreams?

#### Patrick Massot (Apr 28 2020 at 12:59):

Yes, same level

#### Mario Carneiro (Apr 28 2020 at 12:59):

Program verification would be cool, although I think there has been vanishingly small amount of discussion on this topic here

#### Patrick Massot (Apr 28 2020 at 12:59):

Things inside are called topics or threads

#### Patrick Massot (Apr 28 2020 at 12:59):

(Zulip says topic)

#### Patrick Massot (Apr 28 2020 at 13:00):

Mario Carneiro said:

Program verification would be cool, although I think there has been vanishingly small amount of discussion on this topic here

I hope that would help raise this amount

#### Patrick Massot (Apr 28 2020 at 13:00):

Those things are self-sustaining. Program verification is not visible here, hence people don't ask many questions

#### Mario Carneiro (Apr 28 2020 at 13:01):

Should they be default streams? I think last time we found out that it's better to make them default at creation time rather than later

#### Johan Commelin (Apr 28 2020 at 13:01):

Yup, just make things default. that will also help new users

#### Johan Commelin (Apr 28 2020 at 13:01):

It is easier to disable a stream than to discover it

#### Kevin Buzzard (Apr 28 2020 at 13:02):

(deleted)

Last updated: May 14 2021 at 03:27 UTC