emih

I like the story in the article, but I think it tries to create some drama where there isn't any.

I think it's great that a lot of work is done using proof assistants, because clearly it's working out for researchers; diversity of research and of methods is a great strength of science. I really can't see how you can "push it too far", pen-and-paper proofs are not going anywhere. And as more researchers write machine-checked proofs, new techniques for automating these proofs are invented (which is what my research is about hehe) which will only make it easier for more researchers to join in.

> Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean.

_Some_ mathematicians are trying to formalize _some_ of mathematics using a proof assistant called Lean. It's not a new development, proof assistants have been used for decades. Lean 4 has definitely been gaining popularity recently compared to others, but other proof assistants are still very popular.

> a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library

The article makes it sound like there is a single, universal "The Lean Library" that everyone is restricted to. I assume it refers to mathlib? But at the end of the day it's just code and everyone is writing their own libraries, and they can make their own decisions.

Mathematically it's quite pretty, and it gives you elegant partial application for free (at least if you want to partially apply the first N arguments).

I didn't know Standard ML, that's interesting.

And yeah I think this is the way to go. For higher-order functions like map it feels too elegant not to write it in a curried style.

Those are nice examples, thanks.

I was imagining you might achieve this optimization by inlining the function. So if you have

  getClosest(points, p) = findInTree(buildTree(points), p)

And call it like

  myPoints = [...]
  map (getClosest(myPoints, $)) myPoints

Then the compiler might unfold the definition of getClosest and give you

  map (\p -> findInTree(buildTree(myPoints), p)) myPoints

Where it then notices the first part does not depend on p, and rewrite this to

  let tree = buildTree(myPoints) in map (\p -> findInTree(tree, p)) myPoints

Again, pretty contrived example. But maybe it could work.

That's a very good point, I never thought really about how this relates to the execution model & graph reduction and such. Do you have an example of a function where this can make a difference? I might add something to the article about it.

It's also a question of whether this is exclusive to a curried definition or if such an optimization may also apply to partial application with a special operator like in the article. I think it could, but the compiler might need to do some extra work?

Glad to hear the article did what I meant for it to do :)

And yes, another comment mentioned that Scala supports this syntax!

It's not that serious :)

You can still do this though:

  let result = (barbalyze(c, d, $) . foobinade(a, b, $)) input

Or if you prefer left-to-right:

  let result = input
    |> foobinade(a, b, $)
    |> barbalyze(c, d, $)

Maybe what isn't clear is that this hole operator would bind to the innermost function call, not the whole statement.

Thanks for sharing, interesting to see that people writing functional languages also experience the same issues in practice. And they give some reasons I didn't think about.

That's a fair point, they are all isomorphic.

The distinction is mostly semantic so you could say they are the same. But I thought it makes sense to emphasize that the former is a feature of function types, and the latter is still technically single-parameter.

I suppose one real difference is that you cannot feed a tuple into a parameter list function. Like:

fn do_something(name: &str, age: u32) { ... }

let person = ("Alice", 40);

do_something(person); // doesn't compile

Machine learning is definitely enabling writing _proofs_ within a proof assistant, and I'm sure it will help to make formal verification more viable in the future.

Where it cannot (fully) replace humans, is writing the _theorems_ themselves. A human has to check that the theorem being proven is actually what you were trying to prove, and this is not safe from LLM hallucinations. If you ask an LLM, is this bridge safe, and it writes `Theorem bridge_is_safe : 1 + 1 = 2.` and proves this theorem, that does _not_ mean the bridge is safe...

The article then also makes some wild extrapolations:

> We could imagine an LLM assistant for finance that provides an answer only if it can generate a formal proof that it adheres to accounting rules or legal constraints.

I guess it's true because you could imagine this, hypothetically. But it's not going to happen, because you cannot formalize a financial or legal statement in a proof assistant. It's a fundamentally informal, real-world thing, and proof assistants are fundamentally for proving formal, abstract things.

Graph coloring is NP-hard so it would be very difficult to replace it with an O(1) algorithm.

If you mean graph coloring restricted to planar graphs, yes it can always be done with at most 4 colors. But it could still be less, so the answer is not always the same.

(I know it was probably not a very serious comment but I just wanted to infodump about graph theory.)

You can't just put words in the author's mouth.

It's also not true at all. For instance, teaching in primary school is a field that is dominated by women where I live, and I (and I agree with the points described in the article) think it would be great to have more male teachers, so that girls and boys can both have rolemodels when growing up. This would also actually help to solve one of the problems that is described in the article, that boys feel unmotivated in school and fall behind.

The Boost algorithm computes the vertex-biconnected components rather than the edge-biconnected components, which are two different but related concepts. Articulation points are also more related to vertex-biconnectedness than to edge-biconnectedness (articulation points are vertices that lie in multiple vertex-biconnected components, i.e., if you remove one you split up the graph into more components). From what I can see in the Boost docs, it doesn't have an implementation of edge-biconnected components.

You can write an algorithm to compute all of the articulation points & bridges & edge-biconnected components & vertex-biconnected components in a single DFS. Because of this you refer to all of them as just "Tarjan's algorithm" even if you just compute one of them (he is kind of the Euler of graph algorithms in that like half of graph algorithms is named after him). So, on a technical level, I guess my implementation is similar to the algorithm in Boost because they both use DFS and this `low` map, but they compute different things.

Finding the vertex-biconnected components next to the articulation points involves more work though (the implementation I used to have manages to also do it in the same pass but also maintains a stack of edges).

That one is intentional. Note: a tree edge (u, v) is a bridge if and only if low[v] is strictly greater than the entry time of u.

Here 4 is the entry time of that node. (For convenience I made sure that the node labels are just the DFS entry times.)

Though maybe comparing both low values might also work, I'd have to think about that...

Whoops, you got me. Fixed!

At some point I relabeled the vertices to match the DFS order, but I must have forgotten to update this example.

I used to get annoyed by these kinds of questions, but honestly I love talking about things I'm passionate about anyway and I want to get more people interested in the subject. So, I'm happy to answer questions like this and simultaneously sneak in some of my own personal experiences.

Basically you get a bunch of problems (ranging from "check if a number is prime" to complicated graph theoretical problems) and some time to figure them out and code a correct & efficient solution. Often there are computer science concepts and reasoning techniques you need to know about (like biconnected components) to figure out how to make an efficient enough implementation.

The contests I used to go to, you got 11-13 problems and 5 hours to solve them with a team of 3. However, you only have one PC to share, so a lot of the time you are discussing, drawing stuff on paper and figuring out the solution in your head. There is also a printing service during the contest where you can literally get a paper version of your code :) so somebody else can code while you debug on paper.

See for instance https://www.acmicpc.net/category/detail/4319 for the kinds of problems they give (Korean website unfortunately but the problems are in English).