Lean community
Lean and its Mathematical Library # The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura. The community recently switched from using Lean 3 to using Lean 4. This website is still being updated, and some pages have outdated information about Lean 3 (these pages are marked with a prominent banner). The old Lean 3 community website has been archived. The Lean mathem
コロナが変えた『数学科』 - 宇宙の始まり、その確率。
新学期が始まってから はや2ヶ月半，私達はいまコロナと共に生きる方法を身に着けつつあるのではないでしょうか． 私は今年からゼミに所属し，確率論を学び始めました．しかしコロナが大学に及ぼした影響は非常に大きく，『数学科』の今までの環境も変えてしまいました． 今回はその環境の変化について，内部から詳しく述べたいと思います． 2020年6月30日 追記 東大数理科学の院試について新たな情報が得られたので追記しました． 『私の結論』 数学科はコロナの影響が少ない学科の1つであることは間違いないが，数学科のオンライン化はあまり良い影響を生まないだろう． 以下，詳しく述べたいと思います． ゼミ 数学科のゼミは1週間に2,3時間程度というのが一般的かと思います．他の理系学科に比べると恐ろしく少ないですが，数学のゼミというのは準備に何より時間がかかります．次のゼミの準備のために1週間勉強し続けるというのは
未解明だった数学の超難問「ABC予想」を証明 京大の望月教授 斬新・難解で査読に8年 | 毎日新聞
未解明だった数学の超難問「ABC予想」を証明したとする望月新一・京都大数理解析研究所教授（51）の論文が、同所が編集する数学専門誌に掲載されることが決まった。3日、京大が発表した。ABC予想は、素因数分解と足し算・かけ算との関係性を示す命題のこと。4編計646ページからなる論文は、斬新さと難解さから査読（論文の内容チェック）に8年かかったが、その正しさが認められることになった。有名な数学の難問「フェルマーの最終定理」（1995年解決）や「ポアンカレ予想」（2006年解決）の証明などと並ぶ快挙となる。【阿部周一、松本光樹】 望月教授は2012年8月、構想から10年以上かけた「宇宙際タイヒミューラー（IUT）理論」の論文4編を、インターネット上で公開した。これを用いればABC予想など複数の難問が証明できると主張し、大きな注目を集めたが、既存の数学が存立する枠組み（宇宙）を複数考えるという構想は
Scalaプログラマが圏論を学ぶためのオススメ文献 - 3選 - Qiita
圏論は数学の一分野です。これを学ぶのには「数学書」を手に取るのが王道なのですが、残念ながらこれは大部分のプログラマに理解できる言葉では書かれていません。「定義・命題・証明」の積み重ねで書かれています1。ここで大半のScalaプログラマは苦い顔をすると思います。もう少し分かりやすいScalaプログラマ向けの圏論入門がないかと探してみると「Haskell」向けの記事が大量に引っかかるでしょう。ここで多くのScalaプログラマは心を折られてしまいます。「圏論」はまだScalaプログラマには早すぎたんだと・・・ 本記事ではそんなあなたに贈る3つの文献をご紹介したいと思います。 (本記事は自分のブログからの転載記事です。) はじめに 本記事は圏論に興味があるScalaプログラマを対象にしています。特にプログラマにとって実用的な圏論の知識をScalaを通して身につけたい方にオススメします。 プログラマ
プログラマのためのモナド(圏論) / #cat4pg
プログラマのための圏論勉強会 - connpass #cat4pg (Oct 16, 2018) https://cat4pg.connpass.com/event/100728/ YouTube: https://www.youtube.com/watch?v=fhuAlDPgi2Q ---------------------------------------------------------------------------------- ■ 前回 圏論とSwiftへの応用 / iOSDC Japan 2018 - Speaker Deck https://speakerdeck.com/inamiy/iosdc-japan-1 iOSDC Japan 2018 「圏論とSwiftへの応用」発表スライドメモ - Qiita https://qiita.com/inamiy/ite
懸垂線（カテナリー曲線）を考える - Qiita
懸垂線とはあまり伸びないロープやチェーンなどの端を、２点固定してぶら下げてできる曲線です。 これの何が面白いかというと、この曲線が大変シンプルな数式で表せる所にあります。 結論から述べてしまうと以下の式がこの曲線を表現しているというのです。 実際に写真に重ねてみると（desmosは便利ですね！）、 おお、たしかに現実の物理現象と大変よくマッチしています。 実際のところわりとこのトピックは語り尽くされた内容ではありますが、 この記事では、 一体どこからこの関数がやってきたのか？ コンピュータグラフィックスで懸垂線を扱うには？ というのを個人的に興味がある数学と一緒に学んでみたいと思います。 プログラミングにはC++を使うことにします。 この関数はどこから来るの？ 実のところ、この懸垂線の関数の導出には調べてみるとたくさんアプローチがあります。今回はそのうち自分の好きなやり方を一つ紹介します。
"独創的すぎる証明"「ABC予想」をその主張だけでも理解する - アジマティクス
2017年12月16日、数学界に激震が走りました。……というと少し語弊があるでしょうか。 この日、あの「フェルマーの最終定理」に匹敵するとも言われる数学の重要な予想、つまり未解決問題であった「ABC予想」が京都大数理解析研究所の望月新一氏によってついに解決されたというニュースが、数学界を、いや、世界中を駆け巡ったのです。 science.srad.jp とは言っても実は、ABC予想を証明したとする論文は2012年にすでに発表されていて、そこから５年間ずっと「査読中」、つまりその証明が正しいかどうかの検証中だったのです（５年もかかったというのは、それだけこの証明が独創的で難解だったことの証左でもあります）。 端から見ていた所感として、論文が出た当初は、本当にこれがABC予想の証明になっているのか疑う向きも多かったようですが、最近では、証明はほぼ間違いないのだろう、というような雰囲気だったよう
トポロジーへの招待 〜 1. 座標も補助線も使わない「やわらかい幾何学」 - 34歳からの数学博士
この記事は 数学とコンピュータⅡ Advent Calendar 11日目の記事です。 こんにちは、佐野です。12月といえば Advent Calendar の季節です🎄思いつきで 数学とコンピュータ Advent Calendar Ⅰ / Ⅱ を立ち上げたところ、嬉しいことに二つともすぐに満員となりました。エントリーして下さった皆さん、ありがとうございます🙇 僕は全3回でトポロジーの考え方と計算手法を、自作のプログラムを使いながら説明していこうと思います。 座標も補助線も使わない「やわらかい幾何学」 ← イマココ 切り貼りで作る色々な曲面 ... このシリーズを通して トポロジーは最高に自由で楽しい数学（の一つ）である ことをお伝えできたら幸いです！ 「やわらかい幾何学」って何？ 「コーヒーカップを、取っ手の輪っかを残すように変形するとドーナッツの形にできる。従ってコーヒーカップとド
ZOZO Technologies TECH BLOG
2020-04-10 iOS 13から追加されたフルページのスクリーンショットの機能と対応方法の紹介 iOS こんにちは！ ZOZOTOWN部の遠藤です。 iOS 13がリリースされて半年が経ちましたね。iOS 13といえばダークモード機能が注目を浴びましたが、それ以外にもたくさんの新しい機能が追加されました。 本記事では新しく追加されたフルページのスクリーンショットに… iOS 13から追加されたフルページのスクリーンショットの機能と対応方法の紹介 2020-03-13 技術書典 応援祭にて「ZOZO TECH BOOK VOL.1」頒布中 #技術書典 お知らせ こんにちは、ZOZOテクノロジーズ CTO室の池田（@ikenyal）です。 ZOZOテクノロジーズでは、現在開催中の技術書典 応援祭にて、有志で制作した技術同人誌【ZOZO TECH BOOK VOL.1】の頒布を開始しました
ミハイル・レオニドヴィッチ・グロモフ
斬新なアイデアと伝統にとらわれない大胆な数学的手法によって、現代幾何学に新しい局面を切り拓き、多数の難問を解決すると同時に、幾何学、代数学、解析学などの多方面において、これらを統合する新しい視点を提出し、数理科学全般に多大な影響を与えた。 ［受賞当時の対象分野： 数理科学］ グロモフ教授は斬新なアイディアと伝統にとらわれない大胆な数学的手法によって、現代幾何学に新しい局面を切り拓き、多数の難問を解決すると同時に、幾何学、代数学、解析学などの多方面において、これらを統合する新しい視点を提出し、数理科学全般に多大な影響を与えた。 グロモフ教授は、19世紀のリーマンとポアンカレ、20世紀のカルタンとチャーンに続く、現代の幾何学の巨星といえる。幾何学を振り返れば、空間の 大域的な構造と局所的な性質との関係を明らかにすることは、ガウスとリーマンが「空間」の数学的理論を提唱して以来の古くからの中心課題
Knuth multiplicative hash が最小完全ハッシュ関数であることの証明 | メルカリエンジニアリング
こんにちは！サーチチームの @metal_unk です。普段はサーバーサイドエンジニアとして、メルカリの検索を改善する仕事をしています。 メルカリには Be Professional Day という「普段できないことをやろう」をテーマとする日があり、その日は業務に直接関係のないことや、普段は手をつけられないリファクタリングなどがされます。Be Professional Day の様子はこちらで紹介されています。 tech.mercari.com わたしは今回の Be Professional Day で、Knuth multiplicative hash が最小完全ハッシュであることを証明しました。このブログはその証明についての記事です。 「普段できないことをやろう」という Be Professional Day では、証明もアリです。 Knuth multiplicative hash
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
数学の未解決問題「アインシュタイン問題」を“完全解決”する新図形発見 「The hat」を改良
Text to Math Converter
世界の名だたる数学者がこぞって日本のチョークを買い求める理由 : カラパイア
tikzcd-editor
どんな難しい計算や質問にも答えてくれる“WolframAlpha”、日本語版が公開／科学技術計算ソフト「Mathematica」の開発元、Wolfram Researchが運営するサービス
無茶しやがって…。「史上最大の素数」まさかの書籍化
Desmos | Graphing Calculator
31歳からの大学院進学（数学・修士課程） - 34歳からの数学博士
GeoGebra - the world’s favorite, free math tools used by over 100 million students and teachers
