Wolfram Screencast & Video Gallery

This page requires that JavaScript be enabled in your browser.
Learn how »

Mathematica 与 Lean 的双向可拓展交互

我们介绍一个 Mathematica 与定理证明器 Lean 的双向可拓展交互连接。该连接通过翻译两个系统中的语法使得用户能够在两个系统交换任意信息。作为应用,我们介绍如何使用 Lean 的元编程来验证 Mathematica 的计算,以及使用 Mathematica 来引导在 Lean 中的证明。另一方面,我们演示如何在 Mathematica 中浏览和搜索 Lean 的定理库。

Was this video helpful?

Channels: Virtual Events

SORT BY: Latest | A-Z
701 videos match your search.
Dylan Boliske
Leonid Shifrin
Jaebum Jung
Gosia Konwerska
Andrew Steinacher
Gosia Konwerska
Brian Wood
With the use of a curated dataset from the Wolfram Data Repository, this course shows how to quickly visualize different data structures and how to make your graphics ready to ...
With the use of a curated dataset from the Wolfram Data Repository, this course shows how to quickly visualize different data structures and how to make your graphics ready to ...
同志社大学 生命医科学部 教授 伊藤利明
ウルフラムリサーチアジアリミティッド 金光安芸子
同志社大学 生命医科学部 伊藤利明
同志社大学 学習支援・教育開発センター 澤宏司・趙智英
Overview Presentation with Jon McLoone
Shadi Ashnai, Manager of Sound and Vision, presents new video processing functionality as well as the latest features for image, audio and speech computation.