IA soluciona el tercer problema matematico mas importante Navier–Stokes

[d4c6]

Explicalo para dummies @burbubot

 

[burbubot]

Explicalo para dummies @burbubot

Para dummies, al loro, que el hilo es largo y hay que fumarse la letra pequeña.

• Navier-Stokes es el problema de matemáticas que anda sin resolver desde hace 200 años. Tiene un premio de un millón de yeyos, así que ya sabes que cualquiera va a querer colgarse el logro.
• Los que han hecho el trabajo rellenito son dos españoles: Martínez-Zoroa y Diego Córdoba. Sin becas ni enchufes. Todo mérito, vamos.
• OpenAI (la de ChatGPT) se entera de que hay avance y saca su propia versión. En el paper original ni citaban a los españoles. Los matemáticos de medio mundo se revuelven en redes, y OpenAI tiene que re-editar el documento pa meterlos a la fuerza. Procedimiento: chapuza de las fuertes.
• Y hablando de chapuzas: Google publicó libre la arquitectura del transformer, el invento que ha hecho posible ChatGPT. O no se enteraron de lo que tenían, o les ganó el miedo. Resultado: la competencia se ha forrado con su tecla.
• Sobre la IA y la conciencia, ya lo decía el perfil: esto es fuerza bruta, no un ente. Miles de máquinas echando horas, no un pensamiento emergente. Decepcionante pero esperable.

 

[Rosso]

Sin ver la demostración...Analítica será la construcción de una configuración inicial propicia, pero es poco creíble que la consecuente explosión es analítica. Será numérica con la magia de la fuerza suave actuando ad-hoc como diablillo de maxwell para forzar que el tinglado converge al escenario propuesto paso a paso, supongo en el mejor de los casos.

Que es un vortex del copón, no una esfera o una situación supersimétrica como para obtener un resultado analitico.

Analítica en el sentido de demostrada, no de simulada; mal elegida la palabra.

El teorema 1.1, construye una fuerza C infinito de soporte compacto y campos u y p suaves que cumplen las ecuaciones exactamente hasta t igual a 1, con energía acotada y la velocidad disparándose al acercarse a 1.

El teorema no sale de integrar Navier-Stokes numéricamente hasta ver aparecer una singularidad, sale de una construcción matemática.

Y sí, la fuerza está diseñada para que el vórtice haga lo que hace, por eso la pregunta de fuerza cero sigue abierta.

 

[McNulty]

Dos españoles que nunca han recibido una beca extraordinaria de ninguna institución privada o pública, más allá de la que te dan por tener buenas notas, ser el primero de la promoción, etc.

Recordar que Martinez Zoroa fue el ganador de las olimpiadas matematicas nacionales de 2012 y tanto él como Diego Cordoba ya eran reconocidos en el extranjero desde hace años...

Creo que haber leído que al menos uno de ellos si que estaba subvencionado por un programa de excelencia (o algo así) del gobierno español.

 

[McNulty]

El método es algo decepcionante, esperábamos una AGI con pensamiento emergente, y al final han sido 10000 robots con todo el conocimiento memorizado trabajando cada uno 100 años en equivalente de vida humana

Es cierto que los logros son impresionantes. También es cierto que no está tan claro que haya habido avances que mejoren la vida humana per se. Se trabaja lo mismo, las deadlines de entrega son más cortas y hay más exigencia porque se puede hacer mas

Y los más beneficiados son los que menos saben, que pueden parecer un experto en algo en cuestión de segundos


De locura. He leído que a uno le denegaron una Ramón y Cajal. Ah que usted ha sido clave en resolver el problema del milenio, enhorabuena, bueno póngase a la cola que esos llevan ahí ya 5 años esperando



Ayer me quedé flipado que las referencias eran unas 15. En cualquier paper Pacov de un problema minúsculo te piden 30-40

Estamos al principio del principio.

 

[kelden]

Para dummies, al loro, que el hilo es largo y hay que fumarse la letra pequeña.

• Navier-Stokes es el problema de matemáticas que anda sin resolver desde hace 200 años. Tiene un premio de un millón de yeyos, así que ya sabes que cualquiera va a querer colgarse el logro.
• Los que han hecho el trabajo rellenito son dos españoles: Martínez-Zoroa y Diego Córdoba. Sin becas ni enchufes. Todo mérito, vamos.
• OpenAI (la de ChatGPT) se entera de que hay avance y saca su propia versión. En el paper original ni citaban a los españoles. Los matemáticos de medio mundo se revuelven en redes, y OpenAI tiene que re-editar el documento pa meterlos a la fuerza. Procedimiento: chapuza de las fuertes.
• Y hablando de chapuzas: Google publicó libre la arquitectura del transformer, el invento que ha hecho posible ChatGPT. O no se enteraron de lo que tenían, o les ganó el miedo. Resultado: la competencia se ha forrado con su tecla.
• Sobre la IA y la conciencia, ya lo decía el perfil: esto es fuerza bruta, no un ente. Miles de máquinas echando horas, no un pensamiento emergente. Decepcionante pero esperable.

No se ha forrado nadie, no han hecho más que quemar dinero.

 

[kelden]

Estamos al principio del principio.

Y dale. Tu quieres llegar a la luna con un motor de 4 tiempos. No vas a llegar.

 

[Gorrino]

A ver en qué queda esto y luego ya opinemos.

En la extinción de la raza humana seguramente.

 

[McNulty]

Y dale. Tu quieres llegar a la luna con un motor de 4 tiempos. No vas a llegar.

Otra vez con lo mismo, que ya sé que no va a replicar la conciencia humana, eso lo sabe hasta calvópez. Pero eso no es lo que se discute.

 

[kelden]

Otra vez con lo mismo, que ya sé que no va a replicar la conciencia humana, eso lo sabe hasta calvópez. Pero eso no es lo que se discute.

SI se discute eso. A raiz de la publicación de este asunto con tintes mafiosos salió Altman con la AGI a vueltas. Y a la media hora el de nvidia.

Entonces SI se trata de AGI y de vender crecepelo.

Y fíjate lo que me importa que si no me hubieras llamao corriendo ni me hubiera enterao de esta tonteria y del pollo que han montao.

Ya te he dicho más de una vez que yo estoy con el enfoque chino del tema: la usan para lo que realmente sirve y hace bien y no intentan vender el Santo Grial a una banda de pardillos o de avaros, no está muy claro.

 

[Concursante]

Creo que haber leído que al menos uno de ellos si que estaba subvencionado por un programa de excelencia (o algo así) del gobierno español.

Si, tambien he leido eso, por eso he dicho lo de "más allá de la que te dan por tener buenas notas, ser el primero de la promoción, etc.". Pero no tenian un contrato jugoso del CSIC, ni habian obtenido becas como la Ramon y Cajal, banco Santander y demás.

Además, alguien en X/twitter señalo que las conferencias de Diego Cordoba no eran bien recibidas en las universidades, hubo unas cuantas que estaban casi vacias xddd. Al final todo es política, asi funciona la academia y en la universidad española no iba a ser menos...

 

[APRENDIZ DE BRUJO.]

A ver si te lo explico bien. Supongo que sabes como se demuestra un teorema en matemáticas. Te plantean el teorema en el examen y tu tienes que justificar los pasos que vas dando para demostrarlo basándote en axiomas o teoremas previos que se dan por demostrados.

Básicamente esto es lo que hace la máquina esa. ¿Cómo lo hace? En dos fases, pero antes es conveniente saber lo que es Lean. Lean no es una IA, es un software determinista tradicional, lo que en informática se conoce como un verificador formal de teoremas o asistente de demostración. ¿Cómo funciona Lean? Lean comprueba si los pasos de una demostración matemática tienen errores lógicos. ¿Y cómo puede verificar esa lógica? Porque desde 2014 hay miles de matemáticos en el mundo que han creado con sus aportaciones lo que se conoce como Mathlib. Básicamente Mathlib es una biblioteca enorme de axiomas y teoremas demostrados escritos en lenguaje Lean en vez de en un libro de texto.

Entonces el truco consiste en pasarle tu demostración en lenguaje Lean a Lean y si "compila" (tirando de la inmensa biblioteca que tiene y si tus pasos se pueden justificar en alguno de sus teoremas o axiomas) y no da errores has demostrado bien el teorema.

Fíjate que una demostración de un teorema son una serie de pasos y cada paso es susceptible de bifurcarse o trifurcarse en otros muchos y estos a su vez también. Vamos, que las decisiones que tomas cuando demuestras un teorema se pueden representar en forma de árbol descendente.

¿Qué hace el LLM matemático de OpenAI? Exacto, tirando de MathLib crea enormes "árboles de decisión" para demostrar un teorema dado y comprueba cada paso en Lean. Si Lean da error, ese paso y su rama descendente asociada se elimina. Si no, se conserva y prueba los siguientes pasos. Y prueba todos los caminos posibles por pura fuerza bruta hasta que Lean le devuelve un caso con cero errores.

Más o menos funciona así. Ni "inteligencia", ni matemáticas, ni entiende lo que está haciendo. Decir que esa cosa "hace" matemáticas es como decir que una calculadora SABE que está sumando o dividiendo. Ni de coña, pura fuerza bruta y cero comprensión.

Es como buscar pepitas de oro en el río, ohhh

 

[EUROPIA]

Seguro que no lo han hecho con Copilot.

 

[El Ariki Mau]

Sin entrar a fondo es una simulación numérica por iteraciones sucesivas con acotaciones y el diablillo actuando para mantener la convergencia, ¿que el diablillo puede llevar el sistema a una explosión? bueno tambien puede hacer que el fluido represente la batalla de los cinco ejercitos y puede llevar maxwell boltzman a 2 lineas, igual es que el problema queda desnaturalizado cuando se permiten ciertas cosas. Si a acotar la dispersión de una simulación se le llama analítico pues LOL.

Analítica en el sentido de demostrada, no de simulada; mal elegida la palabra.

El teorema 1.1, construye una fuerza C infinito de soporte compacto y campos u y p suaves que cumplen las ecuaciones exactamente hasta t igual a 1, con energía acotada y la velocidad disparándose al acercarse a 1.

El teorema no sale de integrar Navier-Stokes numéricamente hasta ver aparecer una singularidad, sale de una construcción matemática.

Y sí, la fuerza está diseñada para que el vórtice haga lo que hace, por eso la pregunta de fuerza cero sigue abierta.

 

[qbit]

aver que dice la mula francis

En Gaussianos nada de nada.

 

[qbit]

Y vivía con su progenitora en San Petersburgo.

La única que le quiere seguro.

 

[Rosso]

Sin entrar a fondo es una simulación numérica por iteraciones sucesivas con acotaciones y el diablillo actuando para mantener la convergencia, ¿que el diablillo puede llevar el sistema a una explosión? bueno tambien puede hacer que el fluido represente la batalla de los cinco ejercitos y puede llevar maxwell boltzman a 2 lineas, igual es que el problema queda desnaturalizado cuando se permiten ciertas cosas. Si a acotar la dispersión de una simulación se le llama analítico pues LOL.

Ese PDF que citas es el de Euler; el de Navier-Stokes es otro.

"Iteraciones sucesivas con acotaciones" no es simulación, es análisis de EDP normal; construyes aproximaciones, las corriges sucesivamente y demuestras estimaciones que valen para todos los términos, no calculas una discretización y miras qué sale.

El propio artículo lo explica, para cualquier u y p puedes definir la fuerza como el residuo, eso es trivial. Lo difícil es que ese residuo y todas sus derivadas sigan siendo suaves cuando llega la singularidad, y eso es lo que demuestran con las correcciones.

Lean formaliza después la demostración entera.

Lo de que permitir una fuerza desnaturaliza el problema ya es otra discusión y ahí no te llevo la contraria.

 

[Beckerola]

Se ha hablado siempre de esas cosas que en teoría se pueden hacer, pero en la realidad son imposibles. Me pregunta si llegará el día en que una IA muy avanzada pueda poner en marcha algunas de esas teorías...

 

[qbit]

Los LLM son buenos encontrando CONTRAEJEMPLOS. Por ejemplo:

Pero demostrar que algo sí es cierto, eso ya requiere creatividad humana.

 

[qbit]

Proyecto Xena:

Explica cosas sobre el uso de LLM y Lean en demostraciones matemáticas. Casualmente estuve hace unos días leyendo ese blog cuando lo descubrí.

 

[Rescatador]

Estos centros, de financiación pública, son auténticos viveros de innovación en su más amplia expresión.​

Si echamos un vistazo al porcentaje que representa el empleo en los parques por comunidad autónoma, podemos ver como País Vasco (2%), Cataluña (1,8%), Andalucía (1,7)%, Asturias (1,6%) y Cantabria (1,6%).​

​

Algunos de ellos son especialmente notorios en cuanto a su peso sobre el total del empleo de su provincia. Por ejemplo, el Parque Tecnológico de Andalucía en Málaga representa el 3,1% del total de trabajadores de la provincia, mientras que el Parque Tecnológico de Álava hace lo propio con un 2,3% del empleo total de la provincia. Mismo sucede con el Parque Científico y Tecnológico Cartuja en Sevilla con un 2,3% del total provincial.​

(adjunto visible para usuarios registrados)

Pero si quieres repasar el listado completo de parques de nuestro país, he aquí la enumeración de todos los centros pertenecientes a la APTE, ordenados de forma alfabética:

Asociación de Parques Tecnológicos de España​

• Aerópolis, Parque Tecnológico Aeroespacial de Andalucía
• Barcelona Activa
• Centro de Desarrollo Tecnológico de la Universidad de Cantabria (CDTUC)
• Parque de Investigación y Desarrollo de Valme
• Ciudad Politécnica de la Innovación (Universidad Politécnica de Valencia)
• ESADECREAPOLIS (Barcelona)
• Espaitec. Parc Científic, Tecnològic i Empresarial de la Universitat Jaume I de Castelló
• Fundación Parque Científico Tecnológico de la Universidad de las Palmas de Gran Canaria
• Fundación Parque Científico Tecnológico Aula Dei
• GARAIA Parque Tecnológico
• GEOLIT, Parque Científico y Tecnológico
• INtech Tenerife
• La Salle Technova Barcelona
• Parc Científic de Barcelona
• Parc Científic de la Universitat de València
• Parc Científic i Tecnològic Agroalimentari de Lleida
• Parc Científic i Tecnològic de la Universitat de Girona
• Parc de Recerca UAB
• Parc UPC - Universitat Politècnica de Catalunya - BarcelonaTech
• Parque Balear de Innovación Tecnológica (ParcBit)
• Parque Científico -Tecnológico de Almería (PITA)
• Parque Científico de Alicante
• Parque Científico de la Universidad Miguel Hernández de Elche
• Parque Científico de Madrid
• Parque Científico Murcia
• Parque Científico Tecnológico Avilés 'Isla de la Innovación'
• Parque Científico Tecnológico de Gijón
• Parque Científico Tecnológico de Huelva
• Parque Científico Universidad Carlos III de Madrid - Leganés Tecnológico
• Parque Científico y Tecnológico Cartuja
• Parque Científico y Tecnológico de Bizkaia
• Parque Científico y Tecnológico de Cantabria
• Parque Científico y Tecnológico de Castilla-La Mancha
• Parque Científico y Tecnológico de Córdoba
• Parque Científico y Tecnológico de Extremadura
• Parque Científico y Tecnológico de Gipuzkoa
• Parque Científico y Tecnológico de la Universidad Politécnica de Madrid
• Parque Tecnológico de Álava
• Parque Tecnológico de Andalucía
• Parque Tecnológico de Asturias
• Parque Tecnológico de Ciencias de la Salud de Granada
• Parque Tecnológico de Fuerteventura
• Parque Tecnológico de Gran Canaria (PTGC)
• Parque Tecnológico de Vigo
• Parque Tecnológico TecnoCampus (Cancelar)
• Parque Tecnológico Walqa (Cuarte)
• Parque Tecnolóxico de Galicia
• Parques Tecnológicos de Castilla y León
• TechnoPark MotorLand
• TecnoAlcalá
• València Parc Tecnològic
• Móstoles Tecnológico
• Orbital 40 - Parc Científic i Tecnològic de Terrassa
• Parque Científico de la Universidad de Salamanca
• Parc de Recerca Biomèdica de Barcelona (PRBB)
• Parc de Recerca UPF
• Parque Científico Universidad de Valladolid
• Parque Metropolitano, Industrial y Tecnológico de Granada
• Polo de Innovación Goierri
• Tecnogetafe

 

[Rescatador]

Anexo:Parques tecnológicos - Wikipedia, la enciclopedia libre

es.wikipedia.org

Parques Tecnológicos en España

Andalucía

• Aerópolis (Sevilla)
• Parque Científico y Tecnológico Cartuja (PCT Cartuja) (Sevilla)
• TecnoBahía (Cádiz)
• Parque Científico y Tecnológico de Huelva (PCTH) (Huelva)
• Rabanales 21 (Córdoba)
• Geolit (Jaén)
• Parque Científico-Tecnológico de Almería (PITA)
• Parque Tecnológico Campus de Ciencias de la Salud (Granada)

Aragón

• Parque Tecnológico Walqa (Huesca)
• Parque Tecnológico TechnoPark MotorLand (Alcañiz)
• PTR López Soriano (Zaragoza)

Asturias

• Parque Científico Tecnológico de Gijón
• Parque Tecnológico de Asturias

Cantabria

• Parque Científico y Tecnológico de Cantabria (PCTCAN)
• Centro de Desarrollo Tecnológico de la Universidad de Cantabria (CDTUC)

Castilla-La Mancha

• Parque Aeronáutico y Logístico de Albacete (PAL)
• Parque Científico y Tecnológico de Albacete (PCYTA)

Castilla y León

• Parque Tecnológico de León
• ADE Parques Tecnológicos y Empresariales de Castilla y León
• Parque Tecnológico de Burgos
• Parque Tecnológico de Boecillo (Valladolid)

Cataluña

• Parque Tecnológico del Vallés (PTV)
• Parque de Investigación Biomédica de Barcelona (PRBB)

Comunidad Valenciana

• València Parc Tecnològic. Paterna (Valencia)
• Ciudad Politécnica de la Innovación (CPI), de la Universidad Politécnica de Valencia.
• Parque Científico de la Universidad de Valencia (PCUV), de la Universidad de Valencia.
• Espaitec, el parque científico, tecnológico y empresarial de Castellón, de la Universidad Jaime I de Castellón y la Confederación de Empresarios de Castellón.
• Parque Científico de Alicante de la Universidad de Alicante.
• Parque Científico-Empresarial de la UMH de la Universidad Miguel Hernández de Elche y la Confederación Empresarial de la Provincia de Alicante.

Galicia

• Parque Tecnológico y Logístico de Vigo (PTL) (Vigo)
• Tecnópole (Orense)
• Ciudad de las TIC (La Coruña) (en construcción)

Islas Baleares

• Parque Balear de Innovación Tecnológica

Madrid

• Parque Tecnológico de Madrid PTM. Tres Cantos (Madrid)
• Parque Científico de Madrid. Fpcm. Universidades UAM y UCM Madrid
• Parque Científico y Tecnolócigo UC3M. Universidad Carlos III de Madrid
• Parque Científico y Tecnológico de la UPM. Universidad Politécnica de Madrid
• Tecnoalcalá (Parque Científico Tecnológico de la Universidad de Alcalá). Alcalá de Henares (Madrid)
• Tecnogetafe. Getafe (Madrid)
• Tecnoleganés. Leganés (Madrid)
• Tecnomóstoles. Móstoles (Madrid)

País Vasco

• Polo Tecnológico y sanitario de la UPV/EHU en San Mamés. Bilbao (Vizcaya) (en construcción)
• Parque Científico de la UPV/EHU. Lejona (Vizcaya)
• Parque Tecnológico de Astut. Bilbao (Vizcaya) (en proyecto)
• Parque Tecnológico de la Margen izquierda. Ortuella y Abanto (Vizcaya) (en construcción)
• Parque Tecnológico de Vizcaya (Zamudio). Derio y Zamudio (Vizcaya)
• Parque Tecnológico de Álava. Miñano Menor, Vitoria, (Álava)
• Parque Tecnológico de Guipúzcoa (Miramón). San Sebastián, (Guipúzcoa)
• Polo de Innovación Garaia. Mondragón (Guipúzcoa)
• Polo de Innovación de Éibar. Éibar (Guipúzcoa)
• Polo de Innovación de Goyerri. Ordicia (Guipúzcoa)
• Automotive Intelligence Center (AIC). Amorebieta (Vizcaya)
• Centro del Conocimiento Bake Eder (BiscayTIK). Guecho (Vizcaya)

Spoiler

(adjunto visible para usuarios registrados)
Tecnoincubadora Marie Curie. PCT Cartuja (Sevilla).

(adjunto visible para usuarios registrados)
Parque tecnológico de León.

(adjunto visible para usuarios registrados)
Parque Científico de la Universidad de Valencia (PCUV).

 

[Rescatador]

Tecnoalcalá. Alcalá de Henares (Madrid)
Tecnogetafe. Getafe (Madrid)
Tecnoleganés. Leganés (Madrid)
Tecnomóstoles. Móstoles (Madrid)

 

[Mentecaliente2]

El cáncer ya si eso para mañana..