Posted inコンピュータ

Curryのパラドックス

ケプラー予想の証明の概略は下記プレプリントに出ています（査読後出版済み）。 https://arxiv.org/pdf/1501.02155.pdf 証明支援システムは使ったことがないのでわかりませんが、jupyterやgoogle colaboratoryのような、打ち込んで実行した結果が記録されるノート形式の実行環境ではないかと思います。証明は164000行のそういうコードからなるということで、数人のチームで完成に10年かかった、というのは納得できます。上記論文の中には記号論理学で使う記号がたくさん使われています。私は大学1年生のときにゲーデルの不完全性定理を知りたくて記号論理学を履修しま…
Posted inコンピュータ

ケプラー予想と証明支援システム

フランスの研究所INRIAが開発しているCoqは証明支援システムの一種です。windows,macはインストーラーがあるようです。 https://coq.inria.fr/ 大学院集中講義の機械学習講座の付録で「速習python教室」をやることにしたので準備を始めたのですが、「ラムダ式」を調べていたら、本来の目的からずれてこっちに来てしまいました。面白いですが、いまはCoqには深入りできないので、覚書のつもりで「今日の英語」の題材にしています。 さて、数学のいくつかの問題でコンピュータを用いないと証明できない（現状では）ものが知られていて、有名なものの一つは四色問題(四色定理、数百～数千個の…
Posted inコンピュータ 世界の研究所

世界の研究所 フランス Institut National de Recherche en Informatique et en Automatic

フランスで暴動が起こっているようです。今週の世界の研究所は、フランスから、Inistitut National de Recherce en Informatique et en Automatique (INRIA; 国立情報学自動制御研究所）をとりあげます。 https://ja.wikipedia.org/wiki/%E3%83%95%E3%83%A9%E3%83%B3%E3%82%B9%E5%9B%BD%E7%AB%8B%E6%83%85%E5%A0%B1%E5%AD%A6%E8%87%AA%E5%8B%95%E5%88%B6%E5%BE%A1%E7%A0%94%E7%A9%B6%E6…
Posted in本：TheDoorIntoSummer 生物

The Door into Summer(5) 分子進化時計

金曜日は「夏への扉」を読みながら「時間」について考えています。一般相対論のワームホール解、放射壊変の時定数、エントロピーと時間の矢、と来たので、次は遺伝子の話にしましょう。遺伝子は世代を繰り返すと突然変異によって変化し、これが生物の進化と大きく関係してきます。遺伝子の変化は機能を持たない「偽遺伝子」で最も速く、一定値であると考えてよいということが「分子進化の中立説」として正しいとされており、生物の系統がいつ枝分かれしたか、などの時間の推測に使われています。「分子進化時計」と呼ばれます。化学結合論のLinus Pauling が創始者です。　https://en.wikipedia.org/wi…
Posted in技術・工学・物理・数学

CFRPの非破壊検査法

CFRPの非破壊検査に使えそうな方法を調べました。 ●サーモカメラが使えそうです。例えば赤外線などで温めるか、高温の場所においてから室温の場所に持ってきて測ると、温度が高くなったところが見えます。傷があると温度の一様性が損なわれます。 https://www.electronicdesign.com/technologies/embedded/press-release/21211253/ids-imaging-development-systems-nondestructive-testing-of-composite-materials ●ラジオ波のコイルを近づけて電磁誘導を見る論文があり…
Posted in技術・工学・物理・数学

金属疲労の検査法

過酷な環境にさらされる構造物（例：飛行機、橋など）は金属疲労の検査が行われます。通常の金属製品は結晶粒の大きさが1～10ミクロン程度の多結晶の集合体で、変形を繰り返していくと、原子が動くことにより結晶粒が合体して大きくなりながら粒と粒の間に隙間ができて亀裂が成長します。これが金属疲労です。空気中の酸素と反応する金属（銅など）の場合は変形を繰り返すと硬くなってきます。添加物を加えたり、熱処理によって結晶粒の大きさを制御したりするのが冶金（やきん）の技術になります。ジェットエンジンのタービンの羽根（ブレード）など過酷な環境で耐久性が必要な部品は、ブレードの形の鋳型に入れてメートルサイズの単結晶を作…
Posted in技術・工学・物理・数学

鉄筋コンクリートの強度を高めるには鉄筋を引っ張りながら固める

砕けやすい物質に繊維を入れることによって、強度が増すのは鉄筋コンクリートを考えればわかると思います。引っ張る力が均一にかからないで一部に集中することが割れる原因なので、鉄筋を入れることにより力を均一化すれば壊れにくくなります。 コンクリートは引っ張ると割れてしまいますが、押しつぶす力には強いです。そのため、コンクリートが固まるときに鉄筋に引張る力（ひっぱり応力）をかけておいて、固まってから引張をやめると、コンクリートには鉄筋が縮むことにより押しつぶす力がかかります。このようにして作られたコンクリートををprestressed concrete / pre-tensioned concrete …
Posted in世界の研究所 先人 技術・工学・物理・数学

世界の研究所：炭素繊維複合材料発祥の地　通産省大阪工業試験所（現 産総研関西センター）

先週はいろいろなニュースがありました。ロシアの反乱（未遂？）と潜水艇の話が印象的でしたが、今週は潜水艇のほうにしましょう。関係の方々の魂が安らかであることを祈ります。遭難した潜水艇はカーボンファイバー強化プラスチック(carbon fiber reinforced plastics=CFRP)で作られていたという情報があります。今週の世界の研究所は、カーボン複合材の発祥の地(特許1959年)といえる旧・通産省・大阪工業試験所（現：産業技術総合研究所関西センター）を取り上げます。進藤昭男博士の活躍は国立研究所と産業界の連携がうまくいった成功例として知られています。 https://www.ais…
Posted in先人 本：TheDoorIntoSummer

The Door into Summer(4) 時間の矢とエントロピー

金曜日のThe door into summer は第3章です。本文は後にして、時間についての考察を続けましょう。大学1年生に熱力学を教えています。今週はエントロピーの説明をしたら、強い興味を示してくれました。説明がうまくなったから、と言いたいところですが、年によって反応が変わっているだけでしょう（揺らぎの範囲）。私の知らない最近のテレビドラマかマンガでエントロピーが出てきたのかもしれません。さて、熱力学第二法則は「孤立系のエントロピーは増大する」と表現されることがあり、これは「エントロピー」という言葉を作ったClausiusの本に書いてあるそうです。また、エントロピー増大と時間が一方向に流れ…
Posted in企業 技術・工学・物理・数学 物質・化学

医療用同位体を作るサイクロトロンは500億円市場

同位体の放射壊変は医療用にも使われます、PET(positron emission tomography　陽電子放出断層写真法)は、放射壊変して陽電子を出す特定の原子核を含む化合物を人体に注射し、出てきた陽電子が周囲の電子と対消滅するときに180度逆の2方向にガンマ線が出ることを利用して、精度よく人体中の位置を特定できます。転移しているかもしれないガンの場所を探すとき等に威力を発揮します。その時に使う原子核は 18F, 12C, 13N, 15Oで、加速器で作った後迅速に有機合成して糖などの試薬に組み込み注射します。半減期2分のものもあるので、PETには加速器が付属していてその場で原子核を作り…