http://www.stochasticlifestyle.com/when-does-the-mean-and-variance-define-an-sde/
Looks like an open research question still. If someone needs a nice MSc thesis topic or something. 😉
Looks like an open research question still. If someone needs a nice MSc thesis topic or something. 😉
Stochastic Lifestyle
When does the mean and variance define an SDE? - Stochastic Lifestyle
I recently saw a paper that made the following statement: “Innes et al. [22] trained neural SDEs by backpropagating through the operations of the solver, however their training objective simply matched the first two moments of the training data, implying…
https://www.hillelwayne.com/tags/crossover-project/
Хорошие новости для всех, кто (как и я) именует себя "Software Engineer". Да, мы на самом деле можем считаться инженерами!
Более того, накладывать заплатки на заплатки и подпирать костылями -- это старые добрые инженерные традиции. Можно сказать, скрепы.
Но мы можем и лучше. Имеет смысл стараться.
Хорошие новости для всех, кто (как и я) именует себя "Software Engineer". Да, мы на самом деле можем считаться инженерами!
Более того, накладывать заплатки на заплатки и подпирать костылями -- это старые добрые инженерные традиции. Можно сказать, скрепы.
Но мы можем и лучше. Имеет смысл стараться.
👍2
https://behemoth.cl.cam.ac.uk/search/
Natural language based search through Isabelle libraries and AFP for theorems, definitions and alike.
Natural language based search through Isabelle libraries and AFP for theorems, definitions and alike.
https://arxiv.org/abs/1905.05970
HolPy: Interactive Theorem Proving in Python
Bohua Zhan
The code: https://github.com/bzhan/holpy
Yep, they indeed implemented Higher-Order Logic in Python. And a Web interface in Vue. Sounds very hip but actually the interface is pretty nice, suggestions for proof steps are very good. And in general it's very fun to mouse-click your proofs! 😃
HolPy: Interactive Theorem Proving in Python
Bohua Zhan
The code: https://github.com/bzhan/holpy
Yep, they indeed implemented Higher-Order Logic in Python. And a Web interface in Vue. Sounds very hip but actually the interface is pretty nice, suggestions for proof steps are very good. And in general it's very fun to mouse-click your proofs! 😃
GitHub
GitHub - bzhan/holpy: Implementation of higher-order logic in Python
Implementation of higher-order logic in Python. Contribute to bzhan/holpy development by creating an account on GitHub.
В Inria порываются создать пиринговую сеть сертифицированных машинных доказательств: https://www.inria.fr/en/towards-internet-proof
Звучит, конечно, классно, но что-то мне сомнительно, что это будет пользоваться популярностью в обозримом будущем...
Звучит, конечно, классно, но что-то мне сомнительно, что это будет пользоваться популярностью в обозримом будущем...
www.inria.fr
Towards an internet of proof?
In October 2021, Dale Miller, Director of Research at Inria, will launch a new exploratory action that could revolutionise the world of formal proof. The aim is to create a network for sharing documents that certify the validity of computer programs. Using…
🔥1
https://www.hytradboi.com/
Super cool online one-day conference around Databases topics organized by pretty well-known Jamie Brandon. Look at the speakers, there are familiar names too.
Super cool online one-day conference around Databases topics organized by pretty well-known Jamie Brandon. Look at the speakers, there are familiar names too.
https://www.newscientist.com/article/2309566-largest-ever-family-tree-of-humanity-reveals-our-species-history/
Анализируют ДНК останков древних людей, отслеживают пути миграции и расселения. История запутанная, но интересная. Много непонятного, работы для учёных ещё лет на 20 вперёд. 😁
Анализируют ДНК останков древних людей, отслеживают пути миграции и расселения. История запутанная, но интересная. Много непонятного, работы для учёных ещё лет на 20 вперёд. 😁
New Scientist
Largest ever family tree of humanity reveals our species' history
A genealogy of humans constructed from thousands of genomes gives us clues about where our species first evolved and how we spread across the world
https://gmpreussner.com/research/dimensional-analysis-in-programming-languages
Somewhat dated but extremely comprehensive overview of dimensionality analysis (units of measure) problem and solutions in programming languages.
Particularly interesting is a reference to Metaclass extension for Java work devised to support extensible units of measure systems, but seems to be generally applicable to extensible programming. Something to consider for new OO languages developers. 😉
Another curious line of work is inference of units, especially for C. I didn't check but the formal system behind might turn out to be useful for other applications.
The post is kinda obviously lacking an overview of Julia libraries, but I suspect they were written later than the post. 😏
Another major deficiency is the post not even remotely give justice to the great Frink programming language! Most likely the only one practically solving units problem in its entirety. 😁
On the other hand, dimensionality analysis for Excel?!! 😱😂
Somewhat dated but extremely comprehensive overview of dimensionality analysis (units of measure) problem and solutions in programming languages.
Particularly interesting is a reference to Metaclass extension for Java work devised to support extensible units of measure systems, but seems to be generally applicable to extensible programming. Something to consider for new OO languages developers. 😉
Another curious line of work is inference of units, especially for C. I didn't check but the formal system behind might turn out to be useful for other applications.
The post is kinda obviously lacking an overview of Julia libraries, but I suspect they were written later than the post. 😏
Another major deficiency is the post not even remotely give justice to the great Frink programming language! Most likely the only one practically solving units problem in its entirety. 😁
On the other hand, dimensionality analysis for Excel?!! 😱😂
gmpreussner
Dimensional Analysis in Programming Languages | gmpreussner
A survey of existing designs and implementations for automatic conversion and verification of units of measurement in computer programs.
https://yewtu.be/watch?v=IgF3OX8nT0w
This is mind-blowing! Analog computers designed about 100 years before the digital ones by Sir William Thomson, 1st Baron Kelvin himself. And used for pretty much the whole century! Apparently beside all of his numerous contributions to science, Sir Thompson was a Fourier analysis pioneer and popularizer.
More details on Wikipedia: https://en.wikipedia.org/wiki/Tide-predicting_machine
This is mind-blowing! Analog computers designed about 100 years before the digital ones by Sir William Thomson, 1st Baron Kelvin himself. And used for pretty much the whole century! Apparently beside all of his numerous contributions to science, Sir Thompson was a Fourier analysis pioneer and popularizer.
More details on Wikipedia: https://en.wikipedia.org/wiki/Tide-predicting_machine
Корпорация Майкрософт приняла решение глубже локализовать голосового помощника Cortana для России и переименовать его в "Картавый". Активизируется фразой "Слышь, Картавый!"
https://karpathy.github.io/2022/03/14/lecun1989/
Andrej Karpathy "reproduced" seminal Yann LeCun et al. paper " Backpropagation Applied to Handwritten Zip Code Recognition" from 1989 that basically introduced convolutional neural networks to the world. Karpathy's reflections and speculations for the next 33 years are something to think about.
Andrej Karpathy "reproduced" seminal Yann LeCun et al. paper " Backpropagation Applied to Handwritten Zip Code Recognition" from 1989 that basically introduced convolutional neural networks to the world. Karpathy's reflections and speculations for the next 33 years are something to think about.
karpathy.github.io
Deep Neural Nets: 33 years ago and 33 years from now
Musings of a Computer Scientist.
🔥2👍1
https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html
An insightful piece on "types vs. sets" from Lawrence Paulson (of Isabelle fame) himself with rich historical references.
On the other hand it's pretty terse and assumes close familiarity with both Type Theory and Set Theory. And Category Theory for bonus content.
An insightful piece on "types vs. sets" from Lawrence Paulson (of Isabelle fame) himself with rich historical references.
On the other hand it's pretty terse and assumes close familiarity with both Type Theory and Set Theory. And Category Theory for bonus content.
❤1😱1
https://lawrencecpaulson.github.io/2022/03/02/Type_classes.html
If you're not reading Paulson's blog already, here he gives a historical overview of Type Classes from programming languages to proof assistants.
Though keep in mind that in Haskell Multiparam Type Classes are a norm for ages, while Isabelle/HOL only supports Single-parameter Type Classes. I guess this limitation applies to the most of proof assistants.
If you're not reading Paulson's blog already, here he gives a historical overview of Type Classes from programming languages to proof assistants.
Though keep in mind that in Haskell Multiparam Type Classes are a norm for ages, while Isabelle/HOL only supports Single-parameter Type Classes. I guess this limitation applies to the most of proof assistants.
👍1
Paulson's blog is a gift that keeps on giving:
from https://lawrencecpaulson.github.io/2022/02/23/Hereditarily_Finite.html
😄
If you think doing mathematics in a modern proof assistant is difficult, let me remark that doing mathematics in a formalised calculus is a bit like using the kind of proof assistant we had 40 years ago.
from https://lawrencecpaulson.github.io/2022/02/23/Hereditarily_Finite.html
😄
👏1
https://lawrencecpaulson.github.io/2022/02/09/Ackermann-example.html
I guess I just bound to repost almost every Paulson's post, but this one is insanely cool! More about the Ackerman function than you ever thought there is! 😄
I guess I just bound to repost almost every Paulson's post, but this one is insanely cool! More about the Ackerman function than you ever thought there is! 😄
🔥2
https://blog.burntsushi.net/transducers/
Did you know you can use an FSM as a data structure to implement both Sets and Maps? With fuzzy search and regex search? In a streaming fashion so you don't have to keep all of your data in RAM all the time?
Sounds too good to be true? In this somewhat old post Andrew Gallant describes how to do it with references to papers on FSM representation optimization and actual implementation in Rust. Plus some performance benchmarks.
In the last section Andrew discusses major limitations of the approach and some workarounds to partially mitigate them. Also you'll learn that this technique is employed in production inside Lucene and Elastic Search.
Did you know you can use an FSM as a data structure to implement both Sets and Maps? With fuzzy search and regex search? In a streaming fashion so you don't have to keep all of your data in RAM all the time?
Sounds too good to be true? In this somewhat old post Andrew Gallant describes how to do it with references to papers on FSM representation optimization and actual implementation in Rust. Plus some performance benchmarks.
In the last section Andrew discusses major limitations of the approach and some workarounds to partially mitigate them. Also you'll learn that this technique is employed in production inside Lucene and Elastic Search.
burntsushi.net
Index 1,600,000,000 Keys with Automata and Rust - Andrew Gallant's Blog
I blog mostly about my own programming projects.
👍1👎1
Только что позвонили спамеры из компании "Чёрная бухгалтерия". Я не шучу, так и представились: "компания "Чёрная бухгалтерия". 😳
😁1