News for hackers. Stuff that matters.
Re:The Dawn of Formalized Mathematics by dwrensha on Saturday July 03, 2021 @08:37PM (#27726310)
I really like this quote, from 39:50 in the talk:

> This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.

Re:The Dawn of Formalized Mathematics by bookofsand on Sunday July 04, 2021 @02:48AM (#27727744)
Change itself is speeding up. We are going to zoom through the hive era and jump straight into AI era, where 99%, if not more, of the heavy lifting will be done by the machines. The centaur era is rather close ahead. Beyond that, the hope is there will be some room left for humans, but I won't take a long term bet.
Re:The Dawn of Formalized Mathematics by bawolff on Sunday July 04, 2021 @04:34AM (#27728140)
People have been waxing poetic about the singularity for a long time now. I'm not holding my breath.
Re:The Dawn of Formalized Mathematics by habibur on Sunday July 04, 2021 @05:22AM (#27728330)
Neither am I. Had been hearing of downfall of software development since the dawn. Remember 4GL? 4th Generation languages were supposed to end programmer dependency. It will be managers writing what they want in mostly plain English and computer will do the rest.

That was the vision of SQL too. Managers were supposed to write "select sum(amount) from sales where month=2021-05"

Didn't happen. Developers still prefer function calls, ORMs and API calls over English-like sentences. And 4GL has died off like UML.

But things are better now. Getting easier. You don't need to write assembly. And can develop a web page using wordpress without any coding.

But that created a separate class of developers and didn't make seasoned developers out of job. Even though it's been like 20 years since.

Underneath it all there will be people that develop and maintain these AI techs. And as usage rise so will demand for people that can maintain and develop those AI.

Re:The Dawn of Formalized Mathematics by heavenlyblue on Sunday July 04, 2021 @07:30AM (#27728889)
It doesn’t mean it will not happen. For the past 20 years progress in IT was about making IT appear everywhere, that’s a breadth growth rather than depth. Before we need tools that allow someone to program in NLP we need the industry to be broadly used enough to actually have enough data to be manipulated by managers.

On top of this, the company I work for provides amazing tools for non-tech personnel: for example Looker is basically SQL for managers. It is also much more powerful that SQL: for example for simple GROUP BY queries it also provides the UI to access the underlying rows in each of the rows returned by GROUP BY.

You are missing a lot in the industry right now.

Re:The Dawn of Formalized Mathematics by habibur on Sunday July 04, 2021 @08:47AM (#27729242)
> It is also much more powerful that SQL

None of these are new in this decade for that matter. The point is : we are still waiting to see it reduce software engineer's demand overall.

Things are getting easier. Getting more adopted. Leading to increase in demand for software engineers rather than decrease.

Re:The Dawn of Formalized Mathematics by zozbot234 on Monday July 05, 2021 @06:32AM (#27736392)
Query By Example (QBE) is not new. You can do it in Access, ffs.
Re:The Dawn of Formalized Mathematics by pathsjs on Sunday July 04, 2021 @03:28AM (#27727908)
How sad to think of a post industrial division of labour for mathematicians.
Re:The Dawn of Formalized Mathematics by ukj on Sunday July 04, 2021 @05:52AM (#27728464)
Mathematics in isolation is a social anti-pattern.

Individuals keep arriving at the same conclusions, but they invent different notations/languages to express those results. Communication stalls. Tribes form around languages/styles of expression.

It's much much worse than wheel re-inventing too. It takes a very long time to figure out that two Mathematical constructions/notations are equivalent.

It took decades for somebody to notice that proofs are programs.