Pietro Monticone
Pietro Monticone
  • Видео 7
  • Просмотров 5 934
Machine Assisted Proofs | Terence Tao
ABSTRACT
For centuries, mathematicians have relied on computers to perform calculations, to suggest conjectures, and as components of mathematical proofs. In the light of more modern tools such as interactive theorem provers, machine learning algorithms, and generative AI, we are beginning to see machines used in more creative and substantive ways in our work. In this talk we survey some historical and recent developments, and speculate on the future roles of machine assistance in mathematics.
SPEAKER
Terence Tao, University of California Los Angeles
EVENT
ruclips.net/p/PLgBHexwnIcdu8_zggzBpLqp9o1_dALPTZ
Просмотров: 1 477

Видео

The Liquid Tensor Experiment | Kevin Buzzard
Просмотров 9708 месяцев назад
ABSTRACT In December 2020 Peter Scholze raised the question of whether a certain technical result in the Clausen-​Scholze theory of condensed mathematics could be formally verified in an interactive theorem prover. Nineteen months later a team led by Johan Commelin and Adam Topaz showed that the answer was "yes". I'll give a background to the theory of condensed mathematics and will then explai...
What Is an Interactive Theorem Prover? | Kevin Buzzard
Просмотров 8498 месяцев назад
ABSTRACT I will give a live demo of how to use the Lean interactive theorem prover, and discuss uses, and potential future uses, of such tools in teaching, research, and communication of mathematics. LECTURER Kevin Buzzard is Professor of Pure Mathematics at the Imperial College, London. His expertise is in algebraic number theory and he is currently working in the area of formal proof verifica...
Can AI Do Mathematics? | Kevin Buzzard
Просмотров 1,8 тыс.8 месяцев назад
ABSTRACT Large language models like ChatGPT can do all sorts of things - including writing correct computer code. But how good are they at mathematics? Do mathematicians need to start worrying that they will be soon out of a job? More realistically, will we get to the stage where modern computer tools such as large language models and interactive theorem provers will be able to help working mat...
AI to Assist Mathematical Reasoning (Day 3)
Просмотров 140Год назад
ABSTRACT A National Academies of Sciences, Engineering, and Medicine-appointed ad hoc committee will plan and organize a workshop that will bring together academic, industry, and government stakeholders to discuss the state of the art, current challenges, and opportunities to advance research in using AI for mathematical reasoning. This workshop will have a particular focus on exploring approac...
AI to Assist Mathematical Reasoning (Day 2)
Просмотров 214Год назад
ABSTRACT A National Academies of Sciences, Engineering, and Medicine-appointed ad hoc committee will plan and organize a workshop that will bring together academic, industry, and government stakeholders to discuss the state of the art, current challenges, and opportunities to advance research in using AI for mathematical reasoning. This workshop will have a particular focus on exploring approac...
AI to Assist Mathematical Reasoning (Day 1)
Просмотров 463Год назад
ABSTRACT A National Academies of Sciences, Engineering, and Medicine-appointed ad hoc committee will plan and organize a workshop that will bring together academic, industry, and government stakeholders to discuss the state of the art, current challenges, and opportunities to advance research in using AI for mathematical reasoning. This workshop will have a particular focus on exploring approac...

Комментарии

  • @Subliminal8853
    @Subliminal8853 3 месяца назад

    57:00

  • @bobtarmac1828
    @bobtarmac1828 5 месяцев назад

    Ai Hansel and Gretal scenario. Can we …cease Ai? Or else be… laid off by Ai, then human extinction? Or suffer an… Ai new world order? With swell robotics everywhere, …Ai jobloss is the top worry. Anyone else feel the same?

  • @clickaccept
    @clickaccept 5 месяцев назад

    uummm umm uuummmm

  • @양익서-g8j
    @양익서-g8j 5 месяцев назад

    지능은 우주에서 특별하다기보단 보편인식도구일거같음

  • @dadsonworldwide3238
    @dadsonworldwide3238 5 месяцев назад

    Really so many refused cut n dry programs opting for embedded nepotism ai instead of properly innovating along the way because they have no mechanism to push it is an issue. Definable futures of 10 & 20 yrs from now is really where tech oligarchs should stay focused. You can assume anything other than what human infrastructure must do now if we don't get that fine tuned The demand for an army of mathematicians is the better question. . This dictated and defined 1900s structuralism and turned all school into recruiting grounds seeking abstract Euclidean minds with good memorization skills defining our idea of intellect. Ben Franklin dad viewed this as more European opted for a wholistic pragmatic American education so they say. It is a different world for sure. The merit or laborer with an army of mathematicians, physic ,engineers, buyers ,seller all in one domain under one roof where he or she can sub contract out they're skills and trade online is not a bad future if we can obtain it. 60% of us will work for free if that's cheaper than bots. Lol But the means to universal operating systems training on soft& hardware allowing youth to enter the workforce younger as semantics about whatever feild ,diciplines,product or services to be learned in experience along the way isn't bad either. All that matters is syntax, man made time hierarchy knowledge of Good and evil equations x,y z lol

  • @dadsonworldwide3238
    @dadsonworldwide3238 5 месяцев назад

    Idk I think its fair to assume the romantic past when we'll to do aristocracy toiled in sciences when they aren't busy in the farmhouse homesteads but instead of horses you may have cnc lather mills grinders and 3d printers in one stall. Some material sciences working on extracting something needed from that desert sand or salten seas in your region to add local products and services lol To meet new needs new demands. If it's anylitical at all it can computational. As a classical American decendants of a very eccentric fundamentalistic Christian pre separatist pilgrim puritan ,pre mechanics as we know this foresight change them forever lol It's not all bad but 1900s structuralism was a necessary stepping stone period of time and behavior. It took a lot to move ppl off the land to city's to meet factory demands. Those turned into office occupation skyscrapers etc etc. Now they thin.. Once rulers was to relinquish power now it's doctors and mathematicians lol Once only aristocracy or major city's authored history then it was a radical commoners .then a gender. Then a boomer gen a race now it's 8 billion ppl in real time authoring history.

  • @aroundandround
    @aroundandround 5 месяцев назад

    28:44 That’s an easy thing to fix as more recent ChatGPT models already do, by learning the program that needs to be written and executed to actually compute the answer by “thinking”, whatever that means.