News for hackers. Stuff that matters.
Re:Lean 4.0.0, first official lean4 release by kristopolous on Friday September 08, 2023 @09:49AM (#37433468)
It's a quote from a famous book, crossing the chasm and it's a trivial exercise that you're refusing to engage with and mocking me in bad faith, violating HN rules.

The LHC example is so simple ChatGPT did it in a single go. Again, this is generative AI

"For particle physics researchers seeking to unravel the cosmos, the Large Hadron Collider (LHC) offers an unparalleled solution. Unlike conventional particle accelerators, the LHC achieves extraordinary collision energies, enabling experiments that mirror the early universe's conditions. This distinctive feature has led to groundbreaking discoveries, notably the Higgs boson. In contrast to other accelerators, the LHC's unmatched power and global scientific network establish it as the premier choice for unlocking the universe's deepest secrets, setting it apart in its capacity to explore uncharted frontiers in particle physics."

In fact, I asked it to do it for Lean and it could do it just fine.

In contrast, the main lean website starts like this:

The Lean (jargon) is a (jargon) developed principally by Leonardo de Moura.

There's this bizarre fetishism for making things inaccessible and then personally belittling and insulting people when they state the obvious.

The other inexplicable behavior is the tendency to give "answers" by pointing to giant manuals that don't answer the question.

This is endemic to ML. Someone asks what say "Vit-L" versus "Vit-H" means and the answer is usually a link to some ~40 page peer reviewed LaTeX that mentions the acronyms but doesn't define it either.

The strategy is to do anything but be transparent and direct.

Re:Lean 4.0.0, first official lean4 release by uxp8u61q on Friday September 08, 2023 @10:16AM (#37433807)
> "For particle physics researchers seeking to unravel the cosmos, the Large Hadron Collider (LHC) offers an unparalleled solution. Unlike conventional particle accelerators, the LHC achieves extraordinary collision energies, enabling experiments that mirror the early universe's conditions. This distinctive feature has led to groundbreaking discoveries, notably the Higgs boson. In contrast to other accelerators, the LHC's unmatched power and global scientific network establish it as the premier choice for unlocking the universe's deepest secrets, setting it apart in its capacity to explore uncharted frontiers in particle physics."

That's a buzzword soup with barely any actual substance. You're illustrating what I meant. It's also full of jargon (particle accelerators, collision energies, Higgs boson...)

> This is endemic to ML.

Lean and ML are completely unrelated topics.

Re:Lean 4.0.0, first official lean4 release by kristopolous on Friday September 08, 2023 @12:20PM (#37435667)
I'm talking about a culture in mathematics that's intentionally allergic as a matter of custom to effective communication to anyone "outside".

This is so bad that different fields within the discipline can't even understand each other and they wear that as a badge of honor as if being opaque, uninformative, and misleading people is a natural law they're obligated to follow.

It's a truly bizarre social game. A cycle of gaslighting and abuse as an institution.

Re:Lean 4.0.0, first official lean4 release by kristopolous on Friday September 08, 2023 @07:32PM (#37440579)
I had a chance to sleep on this and think it over.

I don't know who goes this deep in to these threads so this is mostly for myself.

My primary critique is from a lifelong love of mathematics. I actually hold a few fancy degrees in the subject.

I cannot stand however, power structures for the sake of power structures. The primary reason I left academia and broke away from the field is my, well, disgust really, with how, I believe willfully obtuse things are.

It's not so much how things are stated although there's problems there, it's the relationship dynamics, interactions, and style of expressions.

Before the rise of the term science, math was called a "natural philosophy" and I really have felt that the mathematics community, at least on the west coast, which is what I've experienced, has an accentuated form of the most off-putting characteristics of philosophy including a steadfast refusal and denial to acknowledge it.

I really think it makes what I consider a beautiful field of study to be hostile, insular and needlessly esoteric.

I still care a lot about it and I want it to be healthier and more open.