> Well, assuming it's free of escape hatches like `sorry`

There are bugs in theorem provers, which means there might be "sorries", maybe even malicious ones (depending on what is at stake), that are not that easy to detect. Personally, I don't think that is much of a problem, as you should be able to come up with a "superlean" version of your theorem prover where correctness is easier to see, and then let the original prover export a proof that the superlean prover can check.

I think more of a concern is that mathematicians might not "understand" the proof anymore that the machine generated. This concern is not about the fact that the proof might be wrong although checked, but that the proof is correct, but cannot be "understood" by humans. I don't think that is too much of a concern either, as we can surely design the machine in a way that the generated proofs are modular, building up beautiful theories on their own.

A final concern might be that what gets lost is that humans understand what "understanding" means. I think that is the biggest concern, and I see it all the time when formalisation is discussed here on HN. Many here think that understanding is simply being able to follow the rules, and that rules are an arbitrary game. That is simply not true. Obviously not, because think about it, what does it mean to "correctly follow the rules"?

I think the way to address this final concern (and maybe the other concerns as well) is to put beauty at the heart of our theorem provers. We need beautiful proofs, written in a beautiful language, checked and created by a beautiful machine.

> Personally, I don't think that is much of a problem, as you should be able to come up with a "superlean" version of your theorem prover where correctness is easier to see, and then let the original prover export a proof that the superlean prover can check.

I think this is sort of how lean itself already works. It has a minimal trusted kernel that everything is forced through. Only the kernel has to be verified.

In principle, this is how these systems work. In practice, there are usually plenty of things that make it difficult to say for sure if you have a proof of something.

Understanding IMO is "developing a correct mental model of a concept". Some heuristics of correctness:

Feynman: "What I cannot build. I do not understand"

Einstein: "If you can't explain it to a six year old, you don't understand it yourself"

Of course none of this changes anything around the machine generated proofs. The point of the proof is to communicate ideas; formalization and verification is simply a certificate showing that those ideas are worth checking out.

Ideas and correctness depend on each other. You usually start with an idea, and check if it is correct. If not, you adjust the idea until it becomes correct. Once you have a correct idea, you can go looking for more ideas based on this.

Formalisation and (formulating) ideas are not separate things, they are both mathematics. In particular, it is not that one should live in Lean, and the other one in blueprints.

Formalisation and verification are not simply certificates. For example, what language are you using for the formalisation? That influences how you can express your ideas formally. The more beautiful your language, the more the formal counter part can look like the original informal idea. This capability might actually be a way to define what it means for a language to be beautiful, together with simplicity.

I share your fascination with proof assistants and formal verification, but the reality is that I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas, or enthusiastic about putting in the actual (additional) work to build the formalization prerequisites to even begin defining the theorem's statement in that (formal) language.

You know what? I agree with you. I have not formalised any of my stuff on abstraction logic [1] for that reason (although that would not be too difficult in Isabelle or Lean), I want to write it down in Practal [2], this becoming possible I see as the first serious milestone for Practal. Eventually, I want Practal to feel more natural than paper, and definitely more natural than LaTeX. That's the goal, and I feel many people now see that this will be possible with AI within the next decade.

[1] http://abstractionlogic.com

[2] https://practal.com

>I am yet to see an actual mathematician working on frontier research who is excited about formalizing their ideas

British mathematician Kevin Buzzard has been evangelizing proof assistants since 2017. I'll leave it to you to decide whether he is working on frontier research:

https://profiles.imperial.ac.uk/k.buzzard/publications

Sure, he is one of biggest advocates for it, and yet he was quite clear that it is not yet possible for him to do his actual research in Lean.

Quoting one of the recent papers (2020):

> With current technology, it would take many person-decades to formalise Scholze’s results. Indeed, even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise the definition of a perfectoid space, and this is what we have done, using the Lean theorem prover.

Thanks for that.

You need to install psycopg2, or perhaps more likely psycopg2-binary to access postgres databases. After hiichbindermax and mrbump helped me out upthread, I was able to get it working via:

    uvx --from sqlit-tui --with psycopg2-binary sqlit

If you're not using uv, then you'll need to install psycopg2-binary in whatever environment you're using (probably via `pip install psycopg2-binary`).

I was surprised to find that I could not run it with uvx:

    % uvx sqlit
       Built unicodecsv==0.14.1
       Built sqlit==0.1.6
    Installed 2 packages in 1ms
    Traceback (most recent call last):
      File "/Users/john/.cache/uv/archive-v0/AP7XgAQ1v0HpPxXUi-hs4/bin/sqlit", line 7, in <module>
        from sqlit.main import main
      File "/Users/john/.cache/uv/archive-v0/AP7XgAQ1v0HpPxXUi-hs4/lib/python3.12/site-packages/sqlit/main.py", line 125
        print sql
        ^^^^^^^^^
    SyntaxError: Missing parentheses in call to 'print'. Did you mean print(...)?

That's not the same package. You should try sqlit-tui

Yes, for uvx you need to do "uvx --from sqlit-tui sqlit"

Ah, thanks. This worked great. I was fooled by the package name.

I think almost everyone is with you on readability, but I think it would be hard to make the case that it lacks power.

Indeed. Read some of the Project Euler discussions (after solving a problem). The J answers tend to be very short and very fast.

They cause hallucinations in dead salmon? I find that hard to believe.

I'm not 100% sure I'd call that a hallucination, but it's close enough and interesting enough that I'm happy to stand corrected.

When improper use of a statistical model generates bogus inferences in generative AI, we call the result a "hallucination"...

I was referring to the dead salmon in the study seeming to show increased activation in the brain and spinal coord.

It should have been called confabulation, hallucination is not the correct analog, tech bros simply used the first word they thought of and it unfortunately stuck.

Undesirable output might be more accurate, since there is absolutely no difference in the process of creating a useful output vs a “hallucination” other than the utility of the resulting data.

I had a partially formed insight along these lines, that LLMs exist in this latent space of information that has so little external grounding. A sort of deeamspace. I wonder if embodying them in robots will anchor them to some kind of ground-truth source?

Loss of consciousness seems equally unlikely.

True, though an easier mistake to make, I imagine.

What is the difference in behavior? They both look like they would delete the user's home directory. I assume the latter would try to delete a directory literally named with a tilde instead?

The latter passes each item in the list into the child processes’s argv, as-is, without the shell parsing them. That means this would delete a single item named “~/ some file”, spaces and all, instead of three items named “~/“, “some”, and “file”.

Edit: I’m typing this on my phone, so brevity won over explicitness. The latter probably wouldn’t expand ~. Imagine a file named “/home/me/ some file” for a better example.

I don't have much need of this personally, but I was playing around with an example from earlier in the thread and ended up with this:

    #!/usr/bin/env -S uv run --with sh --script
    from sh import ifconfig
    print(ifconfig("en0"))

which is a pretty nice experience assuming you already have `uv` in the target environment.

You get all the features of postgres.

QuickCheck also shrinks automatically and preserves invariants though?

Others have pointed out that QuickCheck doesn't shrink automatically. But in addition: QuickCheck's shrinking also doesn't preserve invariants (in general).

QuickCheck's shrinking is type based. There's lots of different ways to generate eg integers. Perhaps you want them in a specific range, or only prime numbers or only even numbers etc. To make QuickCheck's shrinker preserve these invariants, you'd have make a typed wrapper for each of them, and explicitly write a new shrinking strategy. It's annoying and complicated.

Hypothesis does this automatically.

QuickCheck won't preserve invariants, since its shrinkers are separate from its generators. For example:

    data Rat = Rat Int Nat deriving (Eq, Show)

    genRat = do
      (num, den) <- arbitrary
      pure (Rat num (1 + den))

`genRat` is a QuickCheck generator. It cannot do shrinking, because that's a completely separate thing in QuickCheck.

We can write a shrinker for `Rat`, but it will have nothing to do with our generator, e.g.

    shrinkRat (Rat num den) = do
      (num', den') <- shrink (num, den)
      pure (Rat num' den')

Sure, we can stick these in an `Arbitrary` instance, but they're still independent values. The generation process is essentially state-passing with a random number generator; it has nothing to do with the shrinking process, which is a form of search without backtracking.

    instance Arbitrary Rat where
      arbitrary = genRat
      shrink = shrinkRat

In particular, `genRat` satisfies the invariant that values will have non-zero denominator; whereas `shrinkRat` does not satisfy that invariant (since it shrinks the denominator as an ordinary `Nat`, which could give 0). In fact, we can't even think about QuickCheck's generators and shrinkers as different interpretations of the same syntax. For example, here's a shrinker that follows the syntax of `genRat` more closely:

    shrinkRat2 (Rat n d) = do
      (num, den) <- shrink (n, d)
      pure (Rat num (1 + den))

This does have the invariant that its output have non-zero denominators; however, it will get stuck in an infinite loop! That's because the incoming `d` will be non-zero, so when `shrink` tries to shrink `(n, d)`, one of the outputs it tries will be `(n, 0)`; that will lead to `Rat n 1`, which will also shrink to `Rat n 1`, and so on.

In contrast, in Hypothesis, Hedgehog, falsify, etc. a "generator" is just a parser from numbers to values; and shrinking is applied to those numbers, not to the output of a generator. Not only does this not require separate shrinkers, but it also guarantees that the generator's invariants hold for all of the shrunken values; since those shrunken values have also been outputted by the generator (when it was given smaller inputs).

No, QuickCheck very importantly does not shrink automatically. You have to write the shrinker yourself. Hypothesis, Hedgehog, proptest and a few others shrink automatically.

Yes, but instances require the user to provide shrinking while Hypothesis does not: shrinking is derived automatically.

Always returning the empty list meets your spec.

Good point. I suppose we should add "number of input elements equals number of output elements" and "every input element is present in the output". Translated in a straightforward test that still allows my_sort([1,1,2]) to return [1,2,2], but we have to draw the line somewhere

Just use Counter and if the objects aren’t hashable, use the count of IDs. Grab this before calling the function, in case the function is destructive. Check it against the output.

Add in checking each item is less than or equal to its successor and you have the fundamental sort properties. You might have more, like stability.

> we have to draw the line somewhere

Do we? You can pop-count the two lists and checks that those are equal.