Have you ever used the interactive theorem prover Lean?
https://leanprover.github.io/
Thinking about giving it a try. I'm already familiar with Coq, but having native support for quotient types sounds nice.

It seems most people interact with Lean through either VS Code or Emacs. Any thoughts on VS Code? (Obviously I'd want to turn the telemetry off if I went with it.)

Watched /watch?v=POHVMMG7pqE
Was going to comment that the curly brackets look nicer than the Coq +/-/* bullets, but realized that Coq supports the braces too.
Some things that look nice that I don't think Coq has are the TeX to unicode feature and the way it shows the context and unresolved goals in real time when you type out a term with non-inferable "_" placeholders in it. Although these may be more functions of the IDE than of the prover itself.

https://leanprover-community.github.io/install/debian.html
>open a terminal and type:
>
>wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

lovely
but to be fair they say
>If you don't like this method, there is a detailed webpage which will decompose the process into described stages, and won't ask for a blind sudo.

let's look at the detailed webpage
https://leanprover-community.github.io/install/debian_details.html
>curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

>Of course you can get even more details about what is going on by reading the bash script that will be downloaded below: elan_init.
...reading it...
>local _dir="$(mktemp -d 2>/dev/null || ensure mktemp -d -t elan)"
>local _file="$_dir/elan-init$_ext"
...
>ensure curl -sSfL "$ELAN_UPDATE_ROOT/download/$_latest/elan-$_arch.tar.gz" > "$_dir/elan-init.tar.gz"
>(cd "$_dir"; ensure tar xf elan-init.tar.gz; ignore rm elan-init.tar.gz)
...
>ignore "$_file" "$@" < /dev/tty

how deep does it go?
what if you wanted to install this on a machine without network access, what then?

P45118
Seems they learned this from rust:
>elan is basically a fork of rustup.
At least the executable the shell script downloads is nice about explaining what it does and how to uninstall it (at runtime).
https://github.com/leanprover/elan/blob/master/src/elan-cli/self_update.rs
I can't say I like the default behavior of installing software in the user's home directory, though.

Apparently https://vscodium.com/ is built without the telemetry. Or you can build VS Code yourself and there should be no telemetry. The telemetry is only in Microsoft's branded proprietary builds.

P45149
Knowing all the telemetry passed of as "features" that is by default enabled in Firefox I would be shocked if VSCode didn't include 10 000 "security update calls" "add-on safety checking" "Microsoft captive portal service". Simply opening up the add-ons menu should probably pre-fetch 100 .js files from a myriad of Microsoft servers.
I'm guessing this because VSCodium doesn't seem to work well with add-ons or linters, so my guess is hidden telemetry disguised as "features" so they can legally track you and whatnot.

One thing I'll say about the Unicode thing is that I don't like how small ↔ gets when displayed in a monospace font.

These tooltips and the library_search functionality look nice.
Video is /watch?v=b59fpAJ8Mfs

Apparently the default behavior of the recommended leanproject tool is to freshly clone an entire copy of the 723MB-large mathlib library into the _target/deps/mathlib subdirectory of your project. WTF. At least it has the sense to add it to .gitignore. (Although maybe I shouldn't be surprised so much. They seem to be imitating npm's cancer.)

Also
>[dependencies]
>mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "67237461d7cbf410706a6a06f4d40cbb594c32dc"}
Does this thing not have releases with version numbers?

P45153
>VSCodium doesn't seem to work well with add-ons or linters
Fortunately the Lean addon seems to work fine.

P45312
>Does this thing [mathlib] not have releases with version numbers?
Apparently it does not. So I think what I am going to do is pretend they are doing monthly releases by fetching mathlib's last git commit of the previous month (using UTC). I'll also use whatever version of lean that the chosen commit of mathlib said it was using. And if I post anything here, especially if it's a single-file snippet rather than a project, I'll note the lean and mathlib versions in comments at the top of the file, in the same format as they would appear in a leanpkg.toml file.

P45320
Apparently you can set up a file
>~/.lean/leanpkg.path
to tell lean where to look for libraries by default. It doesn't affect lean projects (which would need to use a specific version of mathlib) since they'll have their own leanpkg.path. So I can
>git clone https://github.com/leanprover-community/mathlib
check out the commit I want
and then do
>leanproject get-cache
to download prebuilt .olean files. And then I just point ~/.lean/leanpkg.path at the src subdirectory. The contents of the file looks like this:

builtin_path
path /place/where/mathlib/was/installed/src

>Indeed, if p : Prop is any proposition, Lean’s kernel treats any two elements t1 t2 : p as being definitionally equal, much the same way as it treats (λ x, t)s and t[s/x] as definitionally equal. This is known as proof irrelevance, and is consistent with the interpretation in the last paragraph. It means that even though we can treat proofs t : p as ordinary objects in the language of dependent type theory, they carry no information beyond the fact that p is true.
https://leanprover.github.io/theorem_proving_in_lean/propositions_and_proofs.html

This is another nice thing that fixes what was a pain point when proving things in type theory. The usual way of defining a subtype in type theory is as a pair of objects, one object being of the original type, and the other being a proof that the first object satisfies whatever property you want to hold for the subtype. For example, a natural number less than 5 would consist of a natural number together with a proof that it was less than 5.

The problem: In Coq, it was not necessarily the case that two proofs of the same assertion would be identical. So even if the first elements of a subtype pair were identical, the proofs might not be, so you get two different versions of what's supposed to be the same object. For some statements (3 < 5 is an example), you could prove all the proofs identical, but it was usually complicated. Another hack you could use was to rewrite the propositions as "if boolean_expression then True else False", for which it's easy to prove all proofs identical, but that only works for decidable propositions, propositions where you have an algorithm to test if they're true or false. You could also assume that all proofs of any proposition were equal, but even that is less convenient than the proofs being definitionally equal. More recently, Coq has introduced a fix for this by introducing the SProp sort consisting of propositions whose proofs taken to be definitionally equal.

This notation looks nice. Plus you can use it for operators other than =.

One thing I don't like is how < ⟨ ‹ and > ⟩ › are all used to mean different things.

P47599
update: In practice I've been confusing ⟨⟩ with parentheses () more often.

How long until we see sections like this in every wiki article about math?
https://en.wikipedia.org/wiki/Hilbert%27s_basis_theorem#Formal_proofs

microshit garbage, wake me up when it doesnt force me to use vscrap