欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
灰狐量子实验室
灰狐量子实验室
目录 |
愿景
open science, open research, open institute.
Building a Robust Research Ecosystem.
Huihoo Mathematics Institute.
简介
在当今科学研究中,计算与理论、实验已形成三足鼎立的局面。
目前科学界普遍认为，推动人类文明进步和促进科学技术发展的有三大科学，即理论科学、实验科学和计算科学。
计算科学的发展，产生了一系列诸如：计算数学、计算物理学、计算化学、计算生物学、计算地质学、计算气象学、计算材料学和计算电磁学等学科，逐步形成了一门计算性的学科分支：计算科学与工程（Computational Science and Engineering, CSE）。
灰狐量子实验室专注 灰狐大脑、数学/形式化数学、物理学、光学电学、量子力学、量子计算、编程语言设计/编译器、人工智能/计算语言学/NLP/机器翻译、数论/椭圆曲线/密码学、formal verificcation。
通过类似 Warped Perception 致力于利用科学、工程和技术构建疯狂的项目，揭示和探索各种各样的有趣事物。
编程语言、科学工程、数学物理学、计算机科学、定理证明形式化验证、光学电学、量子计算研究是重点。
打造 Huihoo Brain
成立更多分布式灰狐量子实验室，并协同研究、工作在一起。
并推动 开放大学。
新闻
历史
2022年，数学、物理学、计算机科学即是我们研究、工作的基石和工具，也是我们研究、工作的核心方向和内容。(2022-20??)
2017年，人工智能、大数据和区块链正在重塑世界，接下来10年（2017-2027）靠它们了。
它们是现在和未来商业社会的三大生产要素：
- AI（生产力）
- 大数据（生产资料）
- 区块链（生产关系）
16年前（2000-2016），灰狐通过 JFox、Orbas 等项目发起了开源中间件和灰狐社区。
服务
Compiler, Formal language, Formal mathematics and Formal verification.
数学科学软件是非常有前景和市场的产品领域，有清晰的商业模式。
以 ACL2、Coq、Scilab、GNU Octave、Maxima、SageMath 等开源数学科学软件入手，逐步积累和形成优势。
数学/物理学教学辅导，数值分析/数学科学软件研发与服务，Fortran/Lisp/C++编程语言教育培训咨询，人工神经网络/计算机图形学/计算机视觉/计算语言学相关服务，定理机器证明和形式化验证服务，知识图谱知识管理等。
自由软件
灰狐量子实验室完全基于自由软件构建其基础设施和软件堆栈。
编程语言
编译器技术是计算工业的基石，系统、软件要运行起来都离不开它。
Fortran、Lisp、Haskell、Erlang、C/C++ 是我们的基础和标配语言。
虚拟机也是我们研究的核心方向，如：Erlang VM
我们也尝试设计和实现一个新语言：E language
感兴趣语言还有：
- Erlang/Elixir 并发语言
- Haskell/Agda函数式类型编程语言
- OCaml/Coq functional typed languages
- Smalltalk、Racket 研究教育 STEM 类设计编程语言，桌面、可视化、虚拟机
...
IDE和Editor
通过灰狐量子实验室汇聚更多编程语言爱好者和程序员。
基础设施
Huihoo Cloud 提供基础设施。
私有云
将大数据和人工智能的算力进行私有云化，将 HPCC 和 MXNet 在云端进行深度集成。
大数据
大数据作业通常分为IO密集型（离线数据分析）、计算密集型（在线数据分析）和流计算（实时数据分析）三种。IO密集型指以IO处理为核心作业对象的作业，例如日志分析，数据仓库等，通常使用MapReduce、YARN框架；计算密集型指以内存数据的处理为核心作业对象的作业，例如仿真计算、人工智能等，通常使用Spark框架；流计算通常使用Storm框架对实时数据流进行处理。
- Hortonworks是一个面向数据中心的数据平台，可管理动态数据和静态数据，具备安全性、运营和治理的企业级能力。
- OpenStack Sahara 提供简单部署 Hadoop or Spark on top of OpenStack 的能力，定义BDaaS（BigData as a Service）。
- OpenStack云数据中心的大数据云化演进路线
Sahara应用场景：
- 提供在OpenStack上快速配置和部署大数据集群的能力；
- 充分利用OpenStack IaaS层的计算能力；
- 提供分析即服务（Analyticsas a Service，AaaS）的数据分析业务。
项目
计算机视觉是实验室的核心研究方向：
- TensorFlow和Caffe2是核心项目
- DeepVC
- D3
HPC并行计算
Community building blocks for HPC systems
- Open MPI Open Source High Performance Computing Open MPI @ GitHub
- 并行计算, OpenMP, OpenCL, OpenACC
- OpenHPC, Beowulf
- 超级计算项目为灰狐人工智能实验室提供算力。
- Open Compute Project
- AI accelerator
- PMIx Process Management for Exascale Environments
- Hot Chips A Symposium on High Performance Chips
GPU
- NVIDIA Qwiklabs 实验室
- GPU集群折腾手记 构建自己的GPU集群
FPGA
ARM
- ARM是普适人工智能的核心计算平台
- Hypriot Blog Docker Pirates ARMed with explosive stuff
- ARM Mali GPUs
- Embedded Vision Academy
看听说想
机器人&Bot
一切人工的，都可以智能。
Robot operating system(ROS)是机器人核心操作系统。
OpenBot：开放机器人，实践AI和VA车载语言助手、聊天Bot、告警Bot、虚拟助手等等，每一个设备都住着一位Bot。
操作系统
数学物理
高斯说：“数学是科学的女王”。
数学和物理是灰狐人工智能的基石。
多元微积分、统计与推理、线性代数是学习机器学习的先决条件。
GNU Octave、MATLAB、Julia(Julia Mathematical)、Python和R是核心的数值计算、统计分析语言和软件包。
灰狐D3
D3是一个大数据、机器学习的开源解决方案。
灰狐教育
为灰狐教育提供人工智能服务。
灰狗游戏
为灰狗游戏提供人工智能服务。
- Torch由Lua开发，在Facebook有大量应用。
- Facebook TorchCraft A bridge between Torch and StarCraft.
- DeepMind Lab A customisable 3D platform for agent-based AI research
- OpenAI Universe
- OpenAI and Dota 2
- 阿里巴巴为什么要选择星际争霸作为AI算法研究环境？
打败专业围棋棋手的AI软件：
区块链
- 用人工智能来驱动区块链技术
- 一位AI研究员+区块链创业者的终极展望：AI DAO将统治世界
- 以太坊和Hyperledger Project 超级账本项目的持续跟进
金融资本
组织
文档
图集
万有理论
D-Wave
创新实验室
BitScope Clusters
FPGA系统KV-Direct
ARM生态系统
